Skip to content
Snippets Groups Projects
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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.010May9654329Apr28272625232221201915141312118765431Mar30292825242322211817161110986432128Feb26252423222120191817161514131211109876543129Jan2827Add injectivity result.Should be provable using f_any version.Add alternate forms for results about disjf_any_alt.Use correct witness.More suggestions (transform some defs into inductive types).Tuning exports.Tuning imports.Rename Subset_system_base into Subset_system_base_base.Rename Subset_system_base into Subset_system_base_base.Done.Tuning imports.Split 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...