Documentation Verification Report

SupIndep

📁 Source: Mathlib/Order/SupIndep.lean

Statistics

Metric	Count
Definitions `SupIndep`, `instDecidableSupIndepOfDecidableEq`, `iSupIndep`, `sSupIndep`	4
Theorems `antitone_fun`, `attach`, `biUnion`, `disjoint_sup_sup`, `iSupIndep_of_univ`, `image`, `independent`, `insert`, `le_sup_iff`, `mono`, `pairwiseDisjoint`, `product`, `sigma`, `subset`, `sup`, `union`, `supIndep_attach`, `supIndep_empty`, `supIndep_iff_disjoint_erase`, `supIndep_iff_pairwiseDisjoint`, `supIndep_map`, `supIndep_pair`, `supIndep_product_iff`, `supIndep_sigma_iff'`, `supIndep_singleton`, `supIndep_univ_bool`, `supIndep_univ_fin_two`, `sSupIndep`, `supIndep`, `comp`, `comp'`, `disjoint_biSup`, `injOn`, `injOn_iInf`, `injective`, `map_orderIso`, `mono`, `of_coe_Iic_comp`, `pairwiseDisjoint`, `sSupIndep_range`, `supIndep`, `supIndep'`, `sup_indep_univ`, `iSupIndep_def`, `iSupIndep_def'`, `iSupIndep_def''`, `iSupIndep_empty`, `iSupIndep_iff_pairwiseDisjoint`, `iSupIndep_iff_supIndep`, `iSupIndep_iff_supIndep_univ`, `iSupIndep_map_orderIso_iff`, `iSupIndep_ne_bot`, `iSupIndep_pair`, `iSupIndep_pempty`, `iSupIndep_subsingleton`, `disjoint_sSup`, `mono`, `pairwiseDisjoint`, `sSupIndep_empty`, `sSupIndep_iff`, `sSupIndep_iff_pairwiseDisjoint`, `sSupIndep_pair`, `sSupIndep_singleton`	63
Total	67

Finset

Definitions

Name	Category	Theorems
`SupIndep` 📖	MathDef	21 math math: `Submodule.supIndep_torsionBySet_ideal`, `supIndep_univ_fin_two`, `iSupIndep.supIndep'`, `iSupIndep.supIndep`, `supIndep_iff_pairwiseDisjoint`, `supIndep_empty`, `iSupIndep_iff_supIndep_of_injOn`, `supIndep_product_iff`, `supIndep_pair`, `supIndep_singleton`, `supIndep_sigma_iff'`, `iSupIndep.sup_indep_univ`, `Submodule.supIndep_torsionBy`, `supIndep_map`, `supIndep_iff_disjoint_erase`, `supIndep_univ_bool`, `supIndep_attach`, `Finpartition.supIndep`, `iSupIndep_iff_supIndep`, `iSupIndep_iff_supIndep_univ`, `Set.PairwiseDisjoint.supIndep`
`instDecidableSupIndepOfDecidableEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`supIndep_attach` 📖	mathematical	—	`SupIndep` `Finset` `instMembership` `attach`	—	`attach_map_val` `supIndep_map`
`supIndep_empty` 📖	mathematical	—	`SupIndep` `Finset` `instEmptyCollection`	—	`notMem_empty`
`supIndep_iff_disjoint_erase` 📖	mathematical	—	`SupIndep` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `sup` `Lattice.toSemilatticeSup` `erase`	—	`erase_subset` `notMem_erase` `Disjoint.mono_right` `sup_mono` `mem_erase`
`supIndep_iff_pairwiseDisjoint` 📖	mathematical	—	`SupIndep` `DistribLattice.toLattice` `Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SetLike.coe` `Finset` `instSetLike`	—	`SupIndep.pairwiseDisjoint` `disjoint_sup_right`
`supIndep_map` 📖	mathematical	—	`SupIndep` `map` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`sup_map` `map_subset_map` `mem_map'` `map_eq_image` `SupIndep.image`
`supIndep_pair` 📖	mathematical	—	`SupIndep` `Finset` `instInsert` `instSingleton` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`pair_comm` `erase_insert_eq_erase` `erase_eq_of_notMem` `sup_singleton`
`supIndep_product_iff` 📖	mathematical	—	`SupIndep` `product` `sup` `Lattice.toSemilatticeSup`	—	`sup_image` `sup_product_left` `sup_product_right` `SupIndep.product`
`supIndep_sigma_iff'` 📖	mathematical	—	`SupIndep` `sigma` `sup` `Lattice.toSemilatticeSup`	—	`SupIndep.disjoint_sup_sup` `sup_map` `sup_biUnion` `sup_image` `SupIndep.sigma`
`supIndep_singleton` 📖	mathematical	—	`SupIndep` `Finset` `instSingleton`	—	`eq_empty_of_ssubset_singleton` `sup_empty` `disjoint_bot_right`
`supIndep_univ_bool` 📖	mathematical	—	`SupIndep` `univ` `Bool.fintype` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`supIndep_pair` `disjoint_comm`
`supIndep_univ_fin_two` 📖	mathematical	—	`SupIndep` `univ` `Fin.fintype` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`supIndep_pair`

Finset.SupIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_fun` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.SupIndep`	—	—	`Disjoint.mono` `Finset.sup_mono_fun`
`attach` 📖	mathematical	`Finset.SupIndep`	`Finset` `Finset.instMembership` `Finset.attach`	—	`Finset.supIndep_attach`
`biUnion` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset.biUnion`	—	`Finset.mem_biUnion` `Disjoint.mono_right` `Disjoint.symm` `Disjoint.disjoint_sup_left_of_disjoint_sup_right` `Finset.supIndep_iff_disjoint_erase` `Finset.sup_singleton` `Finset.sup_union`
`disjoint_sup_sup` 📖	mathematical	`Finset.SupIndep` `Finset` `Finset.instHasSubset` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot`	`SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup`	—	`Finset.induction` `Finset.sup_empty`
`iSupIndep_of_univ` 📖	mathematical	`Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder` `Finset.univ`	`iSupIndep`	—	`iSupIndep_iff_supIndep_univ`
`image` 📖	mathematical	`Finset.SupIndep`	`Finset.image`	—	`Finset.subset_image_iff` `Finset.mem_image` `Finset.sup_image` `Finset.mem_image_of_mem`
`independent` 📖	mathematical	`Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder`	`iSupIndep` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`iSupIndep_iff_supIndep`
`insert` 📖	mathematical	`Finset.SupIndep` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset` `Finset.instInsert`	—	—
`le_sup_iff` 📖	mathematical	`Finset.SupIndep` `Finset` `Finset.instHasSubset` `Finset.instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup`	—	`disjoint_self` `Disjoint.mono_right` `Finset.le_sup`
`mono` 📖	—	`Finset.SupIndep` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—	`Disjoint.mono` `Finset.sup_mono_fun`
`pairwiseDisjoint` 📖	mathematical	`Finset.SupIndep`	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.sup_singleton` `Finset.singleton_subset_iff` `Finset.notMem_singleton`
`product` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`SProd.sprod` `Finset` `Finset.instSProd`	—	`Finset.product_eq_biUnion` `biUnion` `Finset.sup_image` `image` `mono` `Finset.le_sup`
`sigma` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset.sigma`	—	`Finset.sigma_eq_biUnion` `biUnion` `Finset.sup_map`
`subset` 📖	—	`Finset.SupIndep` `Finset` `Finset.instHasSubset`	—	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset`
`sup` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.sup_eq_biUnion` `biUnion`
`union` 📖	mathematical	`Finset.SupIndep` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset` `Finset.instUnion`	—	`Finset.biUnion_insert` `Finset.singleton_biUnion`

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sSupIndep` 📖	mathematical	`Set.PairwiseDisjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Order.Frame.toCompleteLattice` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra`	`sSupIndep`	—	`sSupIndep_iff_pairwiseDisjoint`
`supIndep` 📖	mathematical	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.SupIndep`	—	`Finset.supIndep_iff_pairwiseDisjoint`

(root)

Definitions

Name	Category	Theorems
`iSupIndep` 📖	MathDef	47 math math: `Module.End.independent_genEigenspace`, `Module.End.eigenspaces_iSupIndep`, `DirectSum.IsInternal.submodule_iSupIndep`, `DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top`, `iSupIndep_empty`, `Finset.SupIndep.iSupIndep_of_univ`, `iSupIndep_pair`, `LinearIndependent.iSupIndep_span_singleton`, `iSupIndep_of_dfinsuppSumAddHom_injective'`, `iSupIndep_iff_linearIndependent_of_ne_zero`, `Finset.SupIndep.independent`, `sSupIndep_iff`, `iSupIndep_def''`, `Projectivization.independent_iff_iSupIndep`, `iSupIndep_def'`, `iSupIndep_iff_supIndep_of_injOn`, `iSupIndep_pempty`, `iSupIndep_ne_bot`, `iSupIndep_iff_finset_sum_eq_imp_eq`, `Subgroup.independent_of_coprime_order`, `iSupIndep_subsingleton`, `iSupIndep_def`, `HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum'`, `Module.End.independent_maxGenEigenspace`, `iSupIndep_iff_dfinsupp_lsum_injective`, `LieModule.iSupIndep_genWeightSpace`, `iSupIndep_map_orderIso_iff`, `OrthogonalFamily.independent`, `iSupIndep_of_dfinsupp_lsum_injective`, `Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo`, `LieModule.iSupIndep_genWeightSpaceOf`, `iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero`, `AddMonoidHom.independent_range_of_coprime_order`, `DirectSum.IsInternal.addSubgroup_iSupIndep`, `MonoidHom.independent_range_of_coprime_order`, `iSupIndep_iff_supIndep`, `iSupIndep_iff_supIndep_univ`, `LieModule.iSupIndep_genWeightSpace'`, `iSupIndep_range_lsingle`, `LieSubmodule.iSupIndep_toSubmodule`, `iSupIndep_iff_pairwiseDisjoint`, `AddSubgroup.independent_of_coprime_order`, `iSupIndep_iff_dfinsuppSumAddHom_injective`, `DirectSum.IsInternal.addSubmonoid_iSupIndep`, `HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum`, `iSupIndep_iff_forall_dfinsupp`, `iSupIndep_of_dfinsuppSumAddHom_injective`
`sSupIndep` 📖	MathDef	19 math math: `Partition.sSupIndep'`, `Set.PairwiseDisjoint.sSupIndep`, `sSupIndep_iff`, `exists_sSupIndep_isCompl_sSup_atoms`, `sSupIndep_isotypicComponents`, `IsSemisimpleModule.finite_tfae`, `exists_sSupIndep_of_sSup_atoms_eq_top`, `sSupIndep_singleton`, `exists_sSupIndep_disjoint_sSup_atoms`, `sSupIndep_pair`, `Partition.sSupIndep`, `exists_sSupIndep_of_sSup_atoms`, `sSupIndep_iff_finite`, `IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top`, `iSupIndep.sSupIndep_range`, `sSupIndep_iff_pairwiseDisjoint`, `IsSemisimpleModule.exists_linearEquiv_dfinsupp`, `LieAlgebra.IsSemisimple.sSupIndep_isAtom`, `sSupIndep_empty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSupIndep_def` 📖	mathematical	—	`iSupIndep` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—
`iSupIndep_def'` 📖	mathematical	—	`iSupIndep` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.image` `setOf`	—	`sSup_image`
`iSupIndep_def''` 📖	mathematical	—	`iSupIndep` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `setOf`	—	`iSupIndep_def'`
`iSupIndep_empty` 📖	mathematical	—	`iSupIndep`	—	—
`iSupIndep_iff_pairwiseDisjoint` 📖	mathematical	—	`iSupIndep` `Order.Frame.toCompleteLattice` `Pairwise` `Function.onFun` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra`	—	`iSupIndep.pairwiseDisjoint` `disjoint_iSup_iff`
`iSupIndep_iff_supIndep` 📖	mathematical	—	`iSupIndep` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder`	—	`Finset.supIndep_iff_disjoint_erase` `Finset.sup_eq_iSup` `iSup_subtype` `iSup_congr_Prop` `iSup_comm` `iSup_and`
`iSupIndep_iff_supIndep_univ` 📖	mathematical	—	`iSupIndep` `Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder` `Finset.univ`	—	`Finset.sup_eq_iSup` `iSup_congr_Prop`
`iSupIndep_map_orderIso_iff` 📖	mathematical	—	`iSupIndep` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instFunLikeOrderIso`	—	`Function.LeftInverse.comp_eq_id` `Equiv.left_inv` `iSupIndep.map_orderIso`
`iSupIndep_ne_bot` 📖	mathematical	—	`iSupIndep` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`eq_or_ne` `iSup_split` `iSup_subtype` `iSup_congr_Prop` `iSup_comm` `iSup_bot` `sup_of_le_right` `iSupIndep.comp` `Subtype.val_injective`
`iSupIndep_pair` 📖	mathematical	—	`iSupIndep` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder`	—	`iSupIndep.pairwiseDisjoint` `Disjoint.mono_right` `iSup_le` `Eq.le` `Disjoint.symm`
`iSupIndep_pempty` 📖	mathematical	—	`iSupIndep`	—	—
`iSupIndep_subsingleton` 📖	mathematical	—	`iSupIndep`	—	`iSup_congr_Prop` `iSup_neg` `iSup_bot`
`sSupIndep_empty` 📖	mathematical	—	`sSupIndep` `Set` `Set.instEmptyCollection`	—	`Set.notMem_empty`
`sSupIndep_iff` 📖	mathematical	—	`sSupIndep` `iSupIndep` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `iSup_congr_Prop` `iSup_and` `iSup_subtype`
`sSupIndep_iff_pairwiseDisjoint` 📖	mathematical	—	`sSupIndep` `Order.Frame.toCompleteLattice` `Set.PairwiseDisjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra`	—	`sSupIndep.pairwiseDisjoint` `disjoint_sSup_iff`
`sSupIndep_pair` 📖	mathematical	—	`sSupIndep` `Set` `Set.instInsert` `Set.instSingletonSet` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder`	—	`sSupIndep.pairwiseDisjoint` `Set.mem_insert` `Set.mem_insert_of_mem` `Set.mem_singleton` `Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `sSup_singleton` `Set.insert_diff_eq_singleton` `Disjoint.symm`
`sSupIndep_singleton` 📖	mathematical	—	`sSupIndep` `Set` `Set.instSingletonSet`	—	`sdiff_self` `sSup_empty`

iSupIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`iSupIndep`	—	—	`Disjoint.mono_right` `LE.le.trans` `iSup_mono` `iSup_const_mono` `iSup_comp_le`
`comp'` 📖	—	`iSupIndep`	—	—	`Function.Surjective.iSup_comp` `Disjoint.mono_right` `biSup_mono`
`disjoint_biSup` 📖	mathematical	`iSupIndep` `Set` `Set.instMembership`	`Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`Disjoint.mono_right` `biSup_mono`
`injOn` 📖	mathematical	`iSupIndep`	`Set.InjOn` `setOf` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`le_iSup₂` `Disjoint.mono_right` `disjoint_self`
`injOn_iInf` 📖	mathematical	`iSupIndep`	`Set.InjOn` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Function.ne_iff` `le_inf` `iInf_le` `Disjoint.eq_bot` `Disjoint.mono_right` `le_iSup₂_of_le` `le_rfl`
`injective` 📖	—	`iSupIndep`	—	—	`injOn`
`map_orderIso` 📖	mathematical	`iSupIndep`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instFunLikeOrderIso`	—	`Disjoint.mono_right` `Monotone.le_map_iSup₂` `OrderIso.monotone` `Disjoint.map_orderIso`
`mono` 📖	—	`iSupIndep` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	—	`Disjoint.mono` `iSup₂_mono`
`of_coe_Iic_comp` 📖	mathematical	`iSupIndep` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`Set.Iic.instCompleteLattice`	—	`iSup_congr_Prop`
`pairwiseDisjoint` 📖	mathematical	`iSupIndep`	`Pairwise` `Function.onFun` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder`	—	`disjoint_sSup_right` `iSup_pos`
`sSupIndep_range` 📖	mathematical	`iSupIndep`	`sSupIndep` `Set.range`	—	`sSupIndep_iff` `comp'` `Set.coe_comp_rangeFactorization` `Set.rangeFactorization_surjective`
`supIndep` 📖	mathematical	`iSupIndep` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder`	—	`iSupIndep_iff_supIndep`
`supIndep'` 📖	mathematical	`iSupIndep`	`Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder`	—	`supIndep` `comp` `Subtype.coe_injective`
`sup_indep_univ` 📖	mathematical	`iSupIndep`	`Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toBoundedOrder` `Finset.univ`	—	`iSupIndep_iff_supIndep_univ`

sSupIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_sSup` 📖	mathematical	`sSupIndep` `Set` `Set.instMembership` `Set.instHasSubset`	`Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`mono` `Set.insert_subset_iff` `Set.mem_insert` `Set.diff_singleton_eq_self` `Set.insert_diff_of_mem` `Set.mem_singleton`
`mono` 📖	—	`sSupIndep` `Set` `Set.instHasSubset`	—	—	`Disjoint.mono_right` `sSup_le_sSup` `Set.diff_subset_diff_left`
`pairwiseDisjoint` 📖	mathematical	`sSupIndep`	`Set.PairwiseDisjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder`	—	`disjoint_sSup_right` `Set.mem_diff`

---

← Back to Index