Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • Subset
  • essais-8.18
  • master default protected
  • no_ms
  • pr_no_math-comp
  • released
  • test_skolem_ko
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
12 results
Created with Raphaël 2.2.09May654329Apr28272625232221201915141312118765431Mar30292825242322211817161110986432128Feb26252423222120191817161514131211109876543129Jan282726252423222120Would this help when f is of the form (fun A => union A B) for fixed B?Propagate renaming.Fix disj_finite_alt_inter_finite and partition_finite_inter_finite.WIP: fill empty proofs (disj_finite_alt_inter_finite_diffm_seq_r).Use new API.Renaming: unify any/finite/seq (= drop m in subsetm_{finite,seq}_ext*).Renaming: unify any/finite/seq (= drop m in subsetm_{finite,seq}_ext*).Fix, and prove, x_opf_map_any_compose_r.Use new API.Fall back: drop _map in *image{f,p}_map_any, and m in *imagem_seq.Fall back: drop _map in *image{f,p}_map_any, and m in *imagem_seq.Fall back: drop _map in *image{f,p}_map_any, and m in *imagem_seq.Renaming: {,x_}<op>p_any* -> {,x_}<op>p_map_any*, with <op> = op/union/inter/diff/prod.WIP: filling empty proofs about prod and p_any ops.WIP: fix statements and fill empty proofsRenaming: f_fun_any -> f_map_any, f_finite -> m_finite, f_seq -> m_seq.Rename operators on unskolem collections of subsets: *_any* -> *p_any*.Rename compl_seq into complf_seq, and mix_seq into mixf_seq.Rename complf_any into complf_fun_any, and mixf_any into mixf_fun_any.Change order.Change order.Done.Extract todo's into TODO file.Extract todo's into TODO file.WIP: unify any/finite/seq.define cur_to_ref_inv, theta_cur and interp_op_local_cur.WIP: lemma pow_bBijective_bInjective_l...renamed sum_n.v to sum_pn.Vchange sum_n to sum_pn and remove zero case in Finite_dim.vWIP: filling empty proofs.Propagate new API.Renaming: <op>_disj*_compat* -> disj*_<op>*.add sum_pn_scal lemma in sum_n.vMv pb...Renaming: <op>_partition*_compat* -> partition*_<op>*.define vertex_ref from T_geom defWIP: filling empty proofs + some renaming.WIP: filling empty proofs about P-any.try to proof shape_fun_lin_indepmix_any (= union) is useless!