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.010May9654329Apr28272625232221201915141312118765431Mar30292825242322211817161110986432128Feb26252423222120191817161514131211109876543129Jan2827262524Split Sigma_algebra intoDone.Rename Subset_system_{gen,finite,seq,any} into Subset_system_base_{gen,fintie,seq,any}.More to split...Tuning imports.Split Subset_system into _{base,finite,seq,any}.Split Subset_system_def into _{base,finite,seq,any}.Mv.Some doc.Subset_system_def is for definitions.Collect doc.Tuning imports.Done.Tune imports.Hide Topology for the moment...Move FinBij.v into new folder Subset.Move Subset_system.v into new folder Subset_system.Tune imports.Oops, missed to clean that one...Move subset system stuff into new Subset_system folder.Done.Move Subset_*.v into new Subset folder.Mv Subset_def into Subset.Done.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).