Disjointed

📁 Source: Mathlib/Order/Disjointed.lean

Statistics

Metric	Count
Definitions disjointed	1
Theorems disjiUnion_Iic_disjointed, exists_disjointed_le, sup_disjointed, disjointed_succ, disjointed_succ_sup, biUnion_Iic_disjointed, biUnion_Ioc_disjointed_of_monotone, biUnion_range_succ_disjointed, disjoint_disjointed, disjoint_disjointed_of_lt, disjointedRec, disjointed_apply, disjointed_bot, disjointed_eq_inf_compl, disjointed_eq_inter_compl, disjointed_eq_self, disjointed_le, disjointed_le_id, disjointed_of_isMin, disjointed_partialSups, disjointed_subset, disjointed_succ, disjointed_unique, disjointed_unique', disjointed_zero, iSup_disjointed, iUnion_disjointed, partialSups_disjointed, preimage_find_eq_disjointed, sup_Ioc_disjointed_of_monotone	30
Total	31

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjiUnion_Iic_disjointed 📖	mathematical	—	disjiUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder disjointed Finset instGeneralizedBooleanAlgebra Pairwise.set_pairwise Function.onFun Disjoint GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot disjoint_disjointed SetLike.coe instSetLike DFunLike.coe OrderHom SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup instLattice OrderHom.instFunLike partialSups	—	Pairwise.set_pairwise disjoint_disjointed partialSups_disjointed nonempty_Iic partialSups_apply sup'_eq_sup sup_eq_biUnion disjiUnion_eq_biUnion

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_disjointed_le 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra Finset.sup Lattice.toSemilatticeSup GeneralizedBooleanAlgebra.toOrderBot Finset.univ Pairwise Function.onFun Disjoint	—	isEmpty_or_nonempty le_rfl Subsingleton.pairwise IsEmpty.instSubsingleton Equiv.symm_apply_apply disjointed_le Finset.image_univ_equiv sup_disjointed disjoint_disjointed Equiv.injective
sup_disjointed 📖	mathematical	—	Finset.sup Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot Finset.univ disjointed PartialOrder.toPreorder	—	Finset.ext le_rfl Finset.sup_biUnion Finset.sup_congr Finset.nonempty_Iic Finset.sup'_eq_sup partialSups_apply partialSups_disjointed

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjointed_succ 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra IsMax Preorder.toLE	disjointed Order.succ GeneralizedBooleanAlgebra.toSDiff	—	disjointed_succ partialSups_eq
disjointed_succ_sup 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	SemilatticeSup.toMax Lattice.toSemilatticeSup disjointed Order.succ	—	Order.succ_eq_iff_isMax disjointed_le disjointed_apply Finset.ext Order.lt_succ_iff_eq_or_lt_of_not_isMax Finset.nonempty_Iic Finset.sup'_eq_sup partialSups_apply partialSups_eq sdiff_sup_cancel Order.le_succ

(root)

Definitions

Name	Category	Theorems
disjointed 📖	CompOp	43 math math: MeasureTheory.preimage_spanningSetsIndex_singleton, disjointed_eq_self, disjointed_zero, biUnion_range_succ_disjointed, MeasureTheory.spanningSetsIndex_eq_iff, disjointed_eq_inter_compl, sup_Ioc_disjointed_of_monotone, Fintype.sup_disjointed, iUnion_disjointed, disjointed_add_one, disjointed_le_id, partialSups_disjointed, disjoint_disjointed_of_lt, disjointed_unique', Monotone.disjointed_add_one, biUnion_Iic_disjointed, Monotone.disjointed_succ, MeasureTheory.NullMeasurableSet.disjointed, iSup_disjointed, disjointed_le, MeasureTheory.mem_disjointed_spanningSetsIndex, disjointed_of_isMin, MeasureTheory.OuterMeasure.isCaratheodory_disjointed, disjointedRec_zero, disjointed_eq_inf_compl, disjointed_succ, MeasurableSet.disjointed, disjointed_apply, Monotone.disjointed_succ_sup, disjointed_subset, disjoint_disjointed, disjointed_unique, disjointed_bot, preimage_find_eq_disjointed, disjointedRec, partialSups_add_one_eq_sup_disjointed, MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq, disjointed_partialSups, Finset.disjiUnion_Iic_disjointed, MeasureTheory.sum_restrict_disjointed_spanningSets, biUnion_Ioc_disjointed_of_monotone, MeasureTheory.IsSetRing.disjointed_mem, Monotone.disjointed_add_one_sup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_Iic_disjointed 📖	mathematical	—	Set.iUnion Finset Finset.instMembership Finset.Iic PartialOrder.toPreorder disjointed Set BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra DFunLike.coe OrderHom SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike partialSups	—	partialSups_disjointed partialSups_eq_biSup Set.iUnion_congr_Prop
biUnion_Ioc_disjointed_of_monotone 📖	mathematical	Monotone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Preorder.toLE	Set.iUnion Finset Finset.instMembership Finset.Ioc disjointed BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra LocallyFiniteOrder.toLocallyFiniteOrderBot Set.instSDiff	—	Set.iUnion_congr_Prop sup_Ioc_disjointed_of_monotone Finset.sup_set_eq_biUnion
biUnion_range_succ_disjointed 📖	mathematical	—	Set.iUnion Finset Finset.instMembership Finset.range disjointed Set BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike partialSups	—	Nat.range_succ_eq_Iic biUnion_Iic_disjointed
disjoint_disjointed 📖	mathematical	—	Pairwise Function.onFun Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot disjointed PartialOrder.toPreorder DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	pairwise_disjoint_on disjoint_disjointed_of_lt
disjoint_disjointed_of_lt 📖	mathematical	Preorder.toLT	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot disjointed	—	Disjoint.mono_left disjointed_le Finset.le_sup Finset.mem_Iio disjoint_sdiff_self_right
disjointedRec 📖	mathematical	GeneralizedBooleanAlgebra.toSDiff	disjointed	—	disjointed.eq_1 Finset.induction Finset.sup_empty sdiff_bot Finset.sup_insert sup_comm sdiff_sdiff
disjointed_apply 📖	mathematical	—	disjointed GeneralizedBooleanAlgebra.toSDiff Finset.sup Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot Finset.Iio	—	—
disjointed_bot 📖	mathematical	—	disjointed Bot.bot OrderBot.toBot Preorder.toLE	—	disjointed_of_isMin isMin_bot
disjointed_eq_inf_compl 📖	mathematical	—	disjointed BooleanAlgebra.toGeneralizedBooleanAlgebra CompleteBooleanAlgebra.toBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Preorder.toLT Compl.compl BooleanAlgebra.toCompl	—	Finset.sup_eq_iSup iSup_congr_Prop sdiff_eq compl_iSup
disjointed_eq_inter_compl 📖	mathematical	—	disjointed Set BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra Set.instInter Set.iInter Preorder.toLT Compl.compl Set.instCompl	—	disjointed_eq_inf_compl
disjointed_eq_self 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot	disjointed	—	disjointed_apply sdiff_eq_left disjoint_iff Finset.sup_inf_distrib_left Finset.sup_congr Disjoint.symm Finset.mem_Iio Finset.sup_bot
disjointed_le 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra disjointed	—	disjointed_le_id
disjointed_le_id 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra disjointed	—	sdiff_le
disjointed_of_isMin 📖	mathematical	IsMin Preorder.toLE	disjointed	—	Finset.coe_eq_empty Finset.coe_Iio Set.Iio_eq_empty_iff Finset.sup_empty sdiff_bot
disjointed_partialSups 📖	mathematical	—	disjointed PartialOrder.toPreorder DFunLike.coe OrderHom SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra OrderHom.instFunLike partialSups	—	sdiff_eq_symm LE.le.trans sdiff_le le_partialSups Finset.nonempty_Iic partialSups_apply Finset.sup'_eq_sup sdiff_sdiff_eq_sdiff_sup Finset.sup_mono Finset.Iio_subset_Iic_self sup_eq_right Finset.notMem_Iio_self Finset.Iic_eq_cons_Iio Finset.sup_cons sup_sdiff_left_self Finset.ext LE.le.trans_lt le_rfl
disjointed_subset 📖	mathematical	—	Set Set.instHasSubset disjointed BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra	—	disjointed_le
disjointed_succ 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	disjointed Order.succ GeneralizedBooleanAlgebra.toSDiff DFunLike.coe OrderHom SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra OrderHom.instFunLike partialSups	—	disjointed_apply Finset.nonempty_Iic partialSups_apply Finset.sup'_eq_sup Finset.ext Order.lt_succ_iff_of_not_isMax
disjointed_unique 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot partialSups Lattice.toSemilatticeSup PartialOrder.toPreorder	disjointed	—	disjointed_partialSups disjointed_eq_self
disjointed_unique' 📖	mathematical	Pairwise Function.onFun Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot partialSups Lattice.toSemilatticeSup PartialOrder.toPreorder DistribLattice.toLattice instDistribLatticeOfLinearOrder	disjointed	—	disjointed_unique LT.lt.ne
disjointed_zero 📖	mathematical	—	disjointed Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	disjointed_bot
iSup_disjointed 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice disjointed BooleanAlgebra.toGeneralizedBooleanAlgebra CompleteBooleanAlgebra.toBooleanAlgebra PartialOrder.toPreorder	—	iSup_eq_iSup_of_partialSups_eq_partialSups partialSups_disjointed
iUnion_disjointed 📖	mathematical	—	Set.iUnion disjointed Set BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra PartialOrder.toPreorder	—	iSup_disjointed
partialSups_disjointed 📖	mathematical	—	partialSups Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra PartialOrder.toPreorder disjointed	—	Finset.nonempty_Iic Finset.notMem_Iio_self Finset.Iic_eq_cons_Iio Finset.cons.congr_simp Finset.sup'_congr Finset.sup'_eq_sup Finset.sup_cons Finset.sup_empty sdiff_bot lt_or_eq_of_le Finset.ext LE.le.trans_lt le_rfl Finset.sup_biUnion Finset.sup_congr lt_of_lt_of_le Finset.card_cons Finset.card_le_card partialSups_apply sdiff_sup_self OrderHom.ext
preimage_find_eq_disjointed 📖	mathematical	Set Set.instMembership	Set.preimage Nat.find Set.instSingletonSet disjointed BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	Set.ext disjointed_eq_inter_compl
sup_Ioc_disjointed_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra Preorder.toLE	Finset.sup Lattice.toSemilatticeSup GeneralizedBooleanAlgebra.toOrderBot Finset.Ioc disjointed LocallyFiniteOrder.toLocallyFiniteOrderBot GeneralizedBooleanAlgebra.toSDiff	—	LinearLocallyFiniteOrder.instIsSuccArchimedeanOfLocallyFiniteOrder Finset.Ioc_eq_empty_of_le Finset.sup_empty sdiff_self Order.succ_eq_iff_isMax Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax Finset.sup_insert Monotone.disjointed_succ sdiff_sup_sdiff_cancel Order.le_succ

---

← Back to Index