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.09May654329Apr28272625232221201915141312118765431Mar30292825242322211817161110986432128Feb26252423222120191817161514131211109876543129Jan28272625242322Done.Split Subset_def intoRemove empty obsolete file.define f_inv and add preimage_B_eq lemma to prove preimage_correct.Simplify.This is the new definition...Propagate new API.image2_compose_{l,r} generalize x_opp_map_any_compose_r.Move extensionality results about images and preimages to Subset_def.Propagate new API.image2 is more general than x_opp_map_any.Propagate new API.Move basic fun stuff up.Would 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...