Commit 2022-12-29 13:06 b27587b1

View on Github →

feat: port Order.CompleteLatticeIntervals (#1242)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/CompleteLatticeIntervals.lean

added theorem infₛ_within_of_ordConnected

added theorem subset_infₛ_def

added theorem subset_infₛ_of_within

added theorem subset_supₛ_def

added theorem subset_supₛ_of_within

added theorem supₛ_within_of_ordConnected

Modified Mathlib/Order/Monotone/Basic.lean

modified theorem Subtype.mono_coe