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

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