Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-07-14 15:46
bbde7ac2
View on Github →
feat: Extending from
Ici a
(
#5829
)
https://github.com/leanprover-community/mathlib/pull/18795
Estimated changes
Modified
Mathlib/Data/Set/Intervals/ProjIcc.lean
deleted
theorem
Monotone.IccExtend
added
def
Set.IciExtend
added
theorem
Set.IciExtend_apply
added
theorem
Set.IciExtend_coe
added
theorem
Set.IciExtend_of_le
added
theorem
Set.IciExtend_of_mem
added
theorem
Set.IciExtend_self
added
def
Set.IicExtend
added
theorem
Set.IicExtend_apply
added
theorem
Set.IicExtend_coe
added
theorem
Set.IicExtend_of_le
added
theorem
Set.IicExtend_of_mem
added
theorem
Set.IicExtend_self
added
theorem
Set.coe_projIcc
added
theorem
Set.coe_projIci
added
theorem
Set.coe_projIic
added
theorem
Set.iccExtend_apply
added
theorem
Set.monotone_projIci
added
theorem
Set.monotone_projIic
modified
theorem
Set.projIcc_eq_right
added
def
Set.projIci
added
theorem
Set.projIci_coe
added
theorem
Set.projIci_eq_self
added
theorem
Set.projIci_of_le
added
theorem
Set.projIci_of_mem
added
theorem
Set.projIci_self
added
theorem
Set.projIci_surjOn
added
theorem
Set.projIci_surjective
added
def
Set.projIic
added
theorem
Set.projIic_coe
added
theorem
Set.projIic_eq_self
added
theorem
Set.projIic_of_le
added
theorem
Set.projIic_of_mem
added
theorem
Set.projIic_self
added
theorem
Set.projIic_surjOn
added
theorem
Set.projIic_surjective
added
theorem
Set.range_IciExtend
added
theorem
Set.range_IicExtend
added
theorem
Set.range_projIci
added
theorem
Set.range_projIic
added
theorem
Set.strictMonoOn_projIci
added
theorem
Set.strictMonoOn_projIic
added
theorem
StrictMono.strictMonoOn_IciExtend
added
theorem
StrictMono.strictMonoOn_IicExtend