PartialSups

📁 Source: Mathlib/Order/PartialSups.lean

Statistics

Metric	Count
Definitions partialSups, gi	2
Theorems partialSups_eq, partialSups_apply, bddAbove_range_partialSups, ciSup_partialSups_eq, ciSup_partialSups_eq', comp_partialSups, disjoint_partialSups_left, disjoint_partialSups_right, iSup_eq_iSup_of_partialSups_eq_partialSups, iSup_le_iSup_of_partialSups_le_partialSups, iSup_partialSups_eq, le_partialSups, le_partialSups_of_le, map_partialSups, partialSups_apply, partialSups_bot, partialSups_disjoint_of_disjoint, partialSups_eq_biSup, partialSups_eq_biUnion_range, partialSups_eq_ciSup_Iic, partialSups_eq_sUnion_image, partialSups_eq_sup'_range, partialSups_eq_sup_range, partialSups_iff_forall, partialSups_le, partialSups_le_iff, partialSups_mono, partialSups_monotone, partialSups_succ, partialSups_zero, upperBounds_range_partialSups	31
Total	33

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups_eq 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeSup.toPartialOrder	DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	le_antisymm partialSups_le le_partialSups

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups_apply 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder instSemilatticeSup OrderHom.instFunLike partialSups	—	Finset.nonempty_Iic Finset.sup'_apply

(root)

Definitions

Name	Category	Theorems
partialSups 📖	CompOp	57 math math: partialSups_apply, partialSups_const_add, partialSups_succ', partialSups_mono, ciSup_partialSups_eq', Filter.Tendsto.partialSups_apply, partialSups_eq_sup'_range, biUnion_range_succ_disjointed, partialSups_add_one', iSup_partialSups_eq, partialSups_const_mul, partialSups_add_one, disjoint_partialSups_right, ContinuousWithinAt.partialSups_apply, le_partialSups_of_le, comp_partialSups, partialSups_eq_sup_range, partialSups_monotone, disjointed_add_one, partialSups_mul_const, partialSups_succ, partialSups_le, partialSups_disjointed, partialSups_eq_sUnion_image, partialSups_eq_biSup, biUnion_Iic_disjointed, ContinuousWithinAt.partialSups, MeasureTheory.IsSetRing.partialSups_mem, ContinuousOn.partialSups, ciSup_partialSups_eq, ContinuousAt.partialSups, partialSups_zero, map_partialSups, disjoint_partialSups_left, Monotone.partialSups_eq, upperBounds_range_partialSups, partialSups_eq_ciSup_Iic, partialSups_iff_forall, Set.partialSups_eq_accumulate, disjointed_succ, Continuous.partialSups_apply, ContinuousOn.partialSups_apply, MeasureTheory.OuterMeasure.isCaratheodory_partialSups, partialSups_bot, Continuous.partialSups, le_partialSups, partialSups_eq_biUnion_range, partialSups_add_one_eq_sup_disjointed, partialSups_le_iff, bddAbove_range_partialSups, disjointed_partialSups, Filter.Tendsto.partialSups, partialSups_add_const, Finset.disjiUnion_Iic_disjointed, partialSups_disjoint_of_disjoint, ContinuousAt.partialSups_apply, Pi.partialSups_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_range_partialSups 📖	mathematical	—	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Set.range DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	upperBounds_range_partialSups
ciSup_partialSups_eq 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet DFunLike.coe OrderHom SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice OrderHom.instFunLike partialSups	—	LE.le.antisymm ciSup_le partialSups_eq_ciSup_Iic Set.nonempty_Iic_subtype le_ciSup ciSup_mono bddAbove_range_partialSups le_partialSups not_nonempty_iff
ciSup_partialSups_eq' 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice OrderHom.instFunLike partialSups	—	ciSup_partialSups_eq iSup.eq_1 ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove Iff.not bddAbove_range_partialSups
comp_partialSups 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups	—	Finset.nonempty_Iic Finset.sup'_congr map_finset_sup'
disjoint_partialSups_left 📖	mathematical	—	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup OrderHom.instFunLike partialSups	—	partialSups_iff_forall disjoint_sup_left
disjoint_partialSups_right 📖	mathematical	—	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup OrderHom.instFunLike partialSups	—	partialSups_iff_forall disjoint_sup_right
iSup_eq_iSup_of_partialSups_eq_partialSups 📖	mathematical	partialSups Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	—	iSup_partialSups_eq
iSup_le_iSup_of_partialSups_le_partialSups 📖	mathematical	OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Preorder.toLE OrderHom.instPreorder partialSups	ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet	—	iSup_partialSups_eq iSup_mono
iSup_partialSups_eq 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice OrderHom.instFunLike partialSups	—	ciSup_partialSups_eq OrderTop.bddAbove
le_partialSups 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	le_partialSups_of_le le_rfl
le_partialSups_of_le 📖	mathematical	Preorder.toLE	PartialOrder.toPreorder SemilatticeSup.toPartialOrder DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	partialSups_le_iff le_rfl
map_partialSups 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups	—	comp_partialSups
partialSups_apply 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups Finset.sup' Finset.Iic Finset.nonempty_Iic	—	—
partialSups_bot 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Bot.bot OrderBot.toBot Preorder.toLE	—	Finset.coe_Iic Set.Iic_bot Finset.nonempty_Iic Finset.sup'_congr
partialSups_disjoint_of_disjoint 📖	mathematical	Pairwise Function.onFun Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Preorder.toLT	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup OrderHom.instFunLike partialSups	—	disjoint_partialSups_left LT.lt.ne LE.le.trans_lt
partialSups_eq_biSup 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice OrderHom.instFunLike partialSups iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Preorder.toLE	—	iSup_subtype iSup_congr_Prop partialSups_eq_ciSup_Iic
partialSups_eq_biUnion_range 📖	mathematical	—	DFunLike.coe OrderHom Set Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Set.iUnion Finset Finset.instMembership Finset.range	—	partialSups_eq_biSup Set.iUnion_congr_Prop
partialSups_eq_ciSup_Iic 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice OrderHom.instFunLike partialSups iSup Set.Elem Set.Iic ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership	—	le_antisymm Finset.nonempty_Iic Finset.sup'_le le_ciSup_of_le Set.Finite.bddAbove SemilatticeSup.instIsDirectedOrder supSet_to_nonempty Set.finite_range Finite.of_fintype le_rfl ciSup_le Set.nonempty_Iic_subtype Finset.le_sup'
partialSups_eq_sUnion_image 📖	mathematical	—	DFunLike.coe OrderHom Set Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Set.sUnion SetLike.coe Finset Finset.instSetLike Finset.image Finset.range	—	partialSups_eq_biSup Finset.coe_image Finset.coe_range Set.sUnion_image Set.iUnion_congr_Prop
partialSups_eq_sup'_range 📖	mathematical	—	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Finset.sup' Finset.range Finset.nonempty_range_add_one	—	eq_of_forall_ge_iff Finset.nonempty_range_add_one
partialSups_eq_sup_range 📖	mathematical	—	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Finset.sup Finset.range	—	eq_of_forall_ge_iff
partialSups_iff_forall 📖	mathematical	SemilatticeSup.toMax	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups	—	Finset.nonempty_Iic partialSups_apply Finset.comp_sup'_eq_sup'_comp Finset.sup'_eq_sup Finset.inf_eq_iInf iInf_congr_Prop iInf_Prop_eq
partialSups_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	partialSups_le_iff
partialSups_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	partialSups_iff_forall sup_le_iff
partialSups_mono 📖	mathematical	—	Monotone OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Pi.preorder OrderHom.instPreorder partialSups	—	partialSups_le_iff LE.le.trans le_partialSups_of_le
partialSups_monotone 📖	mathematical	—	Monotone PartialOrder.toPreorder SemilatticeSup.toPartialOrder DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	partialSups_le le_partialSups_of_le LE.le.trans
partialSups_succ 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups Order.succ SemilatticeSup.toMax	—	Finset.ext Order.le_succ_iff_eq_or_le le_trans Order.le_succ le_of_eq Finset.nonempty_Iic Finset.mem_singleton_self Finset.sup'_congr Finset.sup'_union
partialSups_zero 📖	mathematical	—	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	partialSups_bot
upperBounds_range_partialSups 📖	mathematical	—	upperBounds Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Set.range DFunLike.coe OrderHom OrderHom.instFunLike partialSups	—	Set.ext le_rfl

partialSups

Definitions

Name	Category	Theorems
gi 📖	CompOp	—

---

← Back to Index