ProjIcc

📁 Source: Mathlib/Order/Interval/Set/ProjIcc.lean

Statistics

Metric	Count
Definitions IccExtend, IciExtend, IicExtend, projIcc, projIci, projIic	6
Theorems IccExtend, IciExtend, IicExtend, IccExtend_apply, IccExtend_eq_self, IccExtend_left, IccExtend_of_le_left, IccExtend_of_mem, IccExtend_of_right_le, IccExtend_range, IccExtend_right, IccExtend_val, IciExtend_apply, IciExtend_coe, IciExtend_of_le, IciExtend_of_mem, IciExtend_self, IicExtend_apply, IicExtend_coe, IicExtend_of_le, IicExtend_of_mem, IicExtend_self, IciExtend, IicExtend, restrict, coe_projIcc, coe_projIci, coe_projIic, monotone_projIcc, monotone_projIci, monotone_projIic, projIcc_eq_left, projIcc_eq_right, projIcc_left, projIcc_of_le_left, projIcc_of_mem, projIcc_of_right_le, projIcc_right, projIcc_surjOn, projIcc_surjective, projIcc_val, projIci_coe, projIci_eq_self, projIci_of_le, projIci_of_mem, projIci_self, projIci_surjOn, projIci_surjective, projIic_coe, projIic_eq_self, projIic_of_le, projIic_of_mem, projIic_self, projIic_surjOn, projIic_surjective, range_IciExtend, range_IicExtend, range_projIcc, range_projIci, range_projIic, strictMonoOn_projIcc, strictMonoOn_projIci, strictMonoOn_projIic, strictMonoOn_IccExtend, strictMonoOn_IciExtend, strictMonoOn_IicExtend	66
Total	72

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IccExtend 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monotone Set.Elem Set.Icc Subtype.preorder Set Set.instMembership	Set.IccExtend	—	comp Set.monotone_projIcc
IciExtend 📖	mathematical	Monotone Set.Elem Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set Set.instMembership	Set.IciExtend	—	comp Set.monotone_projIci
IicExtend 📖	mathematical	Monotone Set.Elem Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set Set.instMembership	Set.IicExtend	—	comp Set.monotone_projIic

Set

Definitions

Name	Category	Theorems
IccExtend 📖	CompOp	17 math math: IccExtend_eq_self, IccExtend_right, IccExtend_of_mem, IccExtend_val, StrictMono.strictMonoOn_IccExtend, Continuous.IccExtend, IccExtend_of_le_left, continuous_IccExtend_iff, ContinuousAt.IccExtend, IccExtend_left, Filter.Tendsto.IccExtend, Monotone.IccExtend, IccExtend_of_right_le, IccExtend_range, IccExtend_apply, Continuous.Icc_extend', ContinuousMap.coe_IccExtend
IciExtend 📖	CompOp	9 math math: range_IciExtend, IciExtend_self, StrictMono.strictMonoOn_IciExtend, OrdConnected.IciExtend, IciExtend_of_le, IciExtend_of_mem, IciExtend_apply, IciExtend_coe, Monotone.IciExtend
IicExtend 📖	CompOp	9 math math: OrdConnected.IicExtend, Monotone.IicExtend, IicExtend_apply, IicExtend_coe, IicExtend_of_le, StrictMono.strictMonoOn_IicExtend, IicExtend_of_mem, range_IicExtend, IicExtend_self
projIcc 📖	CompOp	32 math math: coe_projIcc, mfderivWithin_projIcc_one, projIcc_left, projIcc_of_right_le, mfderivWithin_comp_projIcc_one, unitInterval.symm_projIcc, isQuotientMap_projIcc, LipschitzWith.projIcc, projIcc_eq_one, projIcc_eq_right, abs_projIcc_sub_projIcc, strictMonoOn_projIcc, projIcc_of_mem, projIcc_eq_left, contMDiffWithinAt_comp_projIcc_iff, oneTangentSpaceIcc_def, projIcc_right, mdifferentiableWithinAt_comp_projIcc_iff, monotone_projIcc, projIcc_val, continuous_projIcc, projIcc_surjective, contMDiffOn_comp_projIcc_iff, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, Real.smoothTransition.projIcc, projIcc_surjOn, projIcc_eq_zero, range_projIcc, Real.arcsin_projIcc, contMDiffOn_projIcc, projIcc_of_le_left, ODE.FunSpace.compProj_apply
projIci 📖	CompOp	11 math math: projIci_eq_self, coe_projIci, projIci_surjective, strictMonoOn_projIci, projIci_self, range_projIci, projIci_surjOn, projIci_of_le, projIci_coe, projIci_of_mem, monotone_projIci
projIic 📖	CompOp	11 math math: projIic_surjective, strictMonoOn_projIic, monotone_projIic, projIic_surjOn, projIic_coe, projIic_self, range_projIic, coe_projIic, projIic_of_le, projIic_eq_self, projIic_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IccExtend_apply 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Set instMembership Icc SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin le_max_left max_le min_le_left	—	—
IccExtend_eq_self 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Elem Icc Set instMembership	—	lt_or_ge IccExtend_of_le_left LT.lt.le le_or_gt CanLift.prf Subtype.canLift IccExtend_val IccExtend_of_right_le
IccExtend_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Set instMembership Icc left_mem_Icc	—	IccExtend_of_le_left le_rfl
IccExtend_of_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Set instMembership Icc left_mem_Icc	—	left_mem_Icc projIcc_of_le_left
IccExtend_of_mem 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set instMembership Icc	IccExtend	—	projIcc_of_mem
IccExtend_of_right_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Set instMembership Icc right_mem_Icc	—	right_mem_Icc projIcc_of_right_le
IccExtend_range 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	range IccExtend Elem Icc	—	range_comp range_projIcc image_univ
IccExtend_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Set instMembership Icc right_mem_Icc	—	IccExtend_of_right_le le_rfl
IccExtend_val 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IccExtend Set instMembership Icc	—	projIcc_val
IciExtend_apply 📖	mathematical	—	IciExtend Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup le_max_left	—	—
IciExtend_coe 📖	mathematical	—	IciExtend Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	projIci_coe
IciExtend_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IciExtend Set instMembership Ici le_rfl	—	le_rfl projIci_of_le
IciExtend_of_mem 📖	mathematical	Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IciExtend	—	projIci_of_mem
IciExtend_self 📖	mathematical	—	IciExtend Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder le_rfl	—	IciExtend_of_le le_rfl
IicExtend_apply 📖	mathematical	—	IicExtend Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin min_le_left	—	—
IicExtend_coe 📖	mathematical	—	IicExtend Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	projIic_coe
IicExtend_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IicExtend Set instMembership Iic le_rfl	—	le_rfl projIic_of_le
IicExtend_of_mem 📖	mathematical	Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IicExtend	—	projIic_of_mem
IicExtend_self 📖	mathematical	—	IicExtend Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder le_rfl	—	IicExtend_of_le le_rfl
coe_projIcc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instMembership Icc projIcc SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin	—	—
coe_projIci 📖	mathematical	—	Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIci SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
coe_projIic 📖	mathematical	—	Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIic SemilatticeInf.toMin	—	—
monotone_projIcc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Monotone Elem Icc Subtype.preorder Set instMembership projIcc	—	max_le_max le_rfl min_le_min
monotone_projIci 📖	mathematical	—	Monotone Elem Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set instMembership projIci	—	max_le_max le_rfl
monotone_projIic 📖	mathematical	—	Monotone Elem Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set instMembership projIic	—	min_le_min le_rfl
projIcc_eq_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc LT.lt.le Set instMembership Icc Preorder.toLE left_mem_Icc	—	LT.lt.le left_mem_Icc LT.lt.not_ge
projIcc_eq_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc LT.lt.le Set instMembership Icc Preorder.toLE right_mem_Icc	—	LT.lt.le right_mem_Icc max_min_distrib_left sup_of_le_right LT.lt.not_ge
projIcc_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc Set instMembership Icc left_mem_Icc	—	projIcc_of_le_left le_rfl
projIcc_of_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc Set instMembership Icc left_mem_Icc	—	left_mem_Icc inf_of_le_right LE.le.trans sup_of_le_left
projIcc_of_mem 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set instMembership Icc	projIcc	—	inf_of_le_right sup_of_le_right
projIcc_of_right_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc Set instMembership Icc right_mem_Icc	—	right_mem_Icc inf_of_le_left sup_of_le_right
projIcc_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc Set instMembership Icc right_mem_Icc	—	projIcc_of_right_le le_rfl
projIcc_surjOn 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SurjOn Elem Icc projIcc univ	—	projIcc_val
projIcc_surjective 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Elem Icc projIcc	—	projIcc_val
projIcc_val 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIcc Set instMembership Icc	—	projIcc_of_mem
projIci_coe 📖	mathematical	—	projIci Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	projIci_of_mem
projIci_eq_self 📖	mathematical	—	projIci Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder le_rfl Preorder.toLE	—	le_rfl le_max_left
projIci_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIci Set instMembership Ici le_rfl	—	le_rfl max_eq_left
projIci_of_mem 📖	mathematical	Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIci	—	le_max_left
projIci_self 📖	mathematical	—	projIci Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder le_rfl	—	projIci_of_le le_rfl
projIci_surjOn 📖	mathematical	—	SurjOn Elem Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIci univ	—	projIci_coe
projIci_surjective 📖	mathematical	—	Elem Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIci	—	projIci_coe
projIic_coe 📖	mathematical	—	projIic Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	projIic_of_mem
projIic_eq_self 📖	mathematical	—	projIic Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder le_rfl Preorder.toLE	—	le_rfl min_le_left
projIic_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIic Set instMembership Iic le_rfl	—	le_rfl min_eq_left
projIic_of_mem 📖	mathematical	Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	projIic	—	min_le_left
projIic_self 📖	mathematical	—	projIic Set instMembership Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder le_rfl	—	projIic_of_le le_rfl
projIic_surjOn 📖	mathematical	—	SurjOn Elem Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIic univ	—	projIic_coe
projIic_surjective 📖	mathematical	—	Elem Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIic	—	projIic_coe
range_IciExtend 📖	mathematical	—	range IciExtend Elem Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	range_comp range_projIci image_univ
range_IicExtend 📖	mathematical	—	range IicExtend Elem Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	range_comp range_projIic image_univ
range_projIcc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	range Elem Icc projIcc univ	—	Function.Surjective.range_eq projIcc_surjective
range_projIci 📖	mathematical	—	range Elem Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIci univ	—	Function.Surjective.range_eq projIci_surjective
range_projIic 📖	mathematical	—	range Elem Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder projIic univ	—	Function.Surjective.range_eq projIic_surjective
strictMonoOn_projIcc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictMonoOn Elem Icc Subtype.preorder Set instMembership projIcc	—	projIcc_of_mem
strictMonoOn_projIci 📖	mathematical	—	StrictMonoOn Elem Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set instMembership projIci	—	projIci_of_mem
strictMonoOn_projIic 📖	mathematical	—	StrictMonoOn Elem Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set instMembership projIic	—	projIic_of_mem

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IciExtend 📖	mathematical	—	Set.OrdConnected PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf Set.IciExtend Set.Elem Set.Ici Set Set.instMembership	—	out max_le_max le_rfl
IicExtend 📖	mathematical	—	Set.OrdConnected PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf Set.IicExtend Set.Elem Set.Iic Set Set.instMembership	—	out min_le_min le_rfl
restrict 📖	mathematical	—	Set.OrdConnected Set.Elem Subtype.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership setOf Set.restrict	—	out

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictMonoOn_IccExtend 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder StrictMono Set.Elem Set.Icc Subtype.preorder Set Set.instMembership	StrictMonoOn Set.IccExtend	—	comp_strictMonoOn Set.strictMonoOn_projIcc
strictMonoOn_IciExtend 📖	mathematical	StrictMono Set.Elem Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set Set.instMembership	StrictMonoOn Set.IciExtend	—	comp_strictMonoOn Set.strictMonoOn_projIci
strictMonoOn_IicExtend 📖	mathematical	StrictMono Set.Elem Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set Set.instMembership	StrictMonoOn Set.IicExtend	—	comp_strictMonoOn Set.strictMonoOn_projIic

---

← Back to Index