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`, `disjoint_biSup_biSup'`, `injOn`, `injOn_iInf`, `injective`, `le_iff_eq_of_iSup_eq_top`, `map_orderIso`, `mem_of_biSup_eq_top`, `mono`, `of_coe_Iic_comp`, `pairwiseDisjoint`, `sSupIndep_range`, `supIndep`, `supIndep'`, `sup_indep_univ`, `iSupIndep_comp_coe_iff_supIndep`, `iSupIndep_def`, `iSupIndep_def'`, `iSupIndep_def''`, `iSupIndep_fin_three`, `iSupIndep_iff_pairwiseDisjoint`, `iSupIndep_iff_supIndep_univ`, `iSupIndep_map_orderIso_iff`, `iSupIndep_ne_bot`, `iSupIndep_pair`, `iSupIndep_subsingleton`, `iSup_fin_three`, `disjoint_sSup`, `mono`, `pairwiseDisjoint`, `sSupIndep_empty`, `sSupIndep_iff`, `sSupIndep_iff_pairwiseDisjoint`, `sSupIndep_pair`, `sSupIndep_singleton`	66
Total	70

Finset

Definitions

Name	Category	Theorems
`SupIndep` 📖	MathDef	33 math math: `Submodule.supIndep_torsionBySet_ideal`, `SupIndep.attach`, `SupIndep.product`, `supIndep_univ_fin_two`, `SupIndep.sup`, `SupIndep.mono`, `iSupIndep.supIndep'`, `iSupIndep.supIndep`, `supIndep_iff_pairwiseDisjoint`, `supIndep_empty`, `iSupIndep_comp_coe_iff_supIndep`, `iSupIndep_iff_supIndep_of_injOn`, `SupIndep.image`, `supIndep_product_iff`, `supIndep_pair`, `SupIndep.union`, `supIndep_singleton`, `supIndep_sigma_iff'`, `iSupIndep.sup_indep_univ`, `Submodule.supIndep_torsionBy`, `supIndep_map`, `SupIndep.insert`, `supIndep_iff_disjoint_erase`, `supIndep_univ_bool`, `SupIndep.biUnion`, `supIndep_attach`, `Finpartition.supIndep`, `SupIndep.subset`, `iSupIndep_iff_supIndep`, `iSupIndep_iff_supIndep_univ`, `SupIndep.antitone_fun`, `Set.PairwiseDisjoint.supIndep`, `SupIndep.sigma`
`instDecidableSupIndepOfDecidableEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`supIndep_attach` 📖	mathematical	—	`SupIndep` `Finset` `SetLike.instMembership` `instSetLike` `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` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.SupIndep`	`Finset.SupIndep`	—	`Disjoint.mono` `Finset.sup_mono_fun`
`attach` 📖	mathematical	`Finset.SupIndep`	`Finset.SupIndep` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.attach`	—	`Finset.supIndep_attach`
`biUnion` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset.SupIndep` `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`	`Disjoint` `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.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_comp_coe_iff_supIndep`
`insert` 📖	mathematical	`Finset.SupIndep` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset.SupIndep` `Finset` `Finset.instInsert`	—	—
`le_sup_iff` 📖	mathematical	`Finset.SupIndep` `Finset` `Finset.instHasSubset` `SetLike.instMembership` `Finset.instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`disjoint_self` `Disjoint.mono_right` `Finset.le_sup`
`mono` 📖	mathematical	`Finset.SupIndep` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	`Finset.SupIndep`	—	`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`	`Finset.SupIndep` `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.SupIndep` `Finset.sigma`	—	`Finset.sigma_eq_biUnion` `biUnion` `Finset.sup_map`
`subset` 📖	mathematical	`Finset.SupIndep` `Finset` `Finset.instHasSubset`	`Finset.SupIndep`	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset`
`sup` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset.SupIndep` `Finset.sup` `Finset` `Lattice.toSemilatticeSup` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.sup_eq_biUnion` `biUnion`
`union` 📖	mathematical	`Finset.SupIndep` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup`	`Finset.SupIndep` `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` `Order.Frame.toCompleteLattice`	—	`sSupIndep_iff_pairwiseDisjoint`
`supIndep` 📖	mathematical	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.SupIndep` `DistribLattice.toLattice`	—	`Finset.supIndep_iff_pairwiseDisjoint`

(root)

Definitions

Name	Category	Theorems
`iSupIndep` 📖	MathDef	55 math math: `Module.End.independent_genEigenspace`, `Module.End.eigenspaces_iSupIndep`, `DirectSum.IsInternal.submodule_iSupIndep`, `LinearMap.iSupIndep_map`, `DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top`, `iSupIndep.mono`, `Finset.SupIndep.iSupIndep_of_univ`, `iSupIndep.comp`, `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`, `LieAlgebra.Basis.iSupIndep_rootSpace`, `iSupIndep_def'`, `iSupIndep_comp_coe_iff_supIndep`, `iSupIndep_iff_supIndep_of_injOn`, `iSupIndep_ne_bot`, `iSupIndep_iff_finset_sum_eq_imp_eq`, `iSupIndep.comp'`, `Subgroup.independent_of_coprime_order`, `iSupIndep_subsingleton`, `iSupIndep_def`, `HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum'`, `iSupIndep.of_coe_Iic_comp`, `iSupIndep.iInf`, `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`, `iSupIndep_fin_three`, `iSupIndep.map_orderIso`, `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	22 math math: `iSupIndep_sUnion_of_directed`, `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.mono`, `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`, `sSupIndep_iUnion_of_directed`, `IsSemisimpleModule.exists_linearEquiv_dfinsupp`, `LieAlgebra.IsSemisimple.sSupIndep_isAtom`, `sSupIndep_empty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSupIndep_comp_coe_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_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_fin_three` 📖	mathematical	—	`iSupIndep` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`iSupIndep_def` `sup_comm` `iSup_fin_three` `iSup_congr_Prop` `iSup_neg` `iSup_pos` `sup_of_le_right` `sup_of_le_left` `Fintype.complete`
`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_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_subsingleton` 📖	mathematical	—	`iSupIndep`	—	`iSup_congr_Prop` `iSup_neg` `iSup_bot`
`iSup_fin_three` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`Finset.sup_eq_iSup` `Finset.sup_insert` `Finset.sup_singleton` `sup_assoc` `iSup_congr_Prop` `iSup_pos`
`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` 📖	mathematical	`iSupIndep`	`iSupIndep`	—	`Disjoint.mono_right` `LE.le.trans` `iSup_mono` `iSup_const_mono` `iSup_comp_le`
`comp'` 📖	mathematical	`iSupIndep`	`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` `Set` `Set.instMembership`	—	`Disjoint.mono_right` `biSup_mono`
`disjoint_biSup_biSup'` 📖	mathematical	`iSupIndep` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`Finset.induction_on` `iSup_congr_Prop` `iSup_neg` `iSup_bot` `Finset.coe_insert` `iSup_insert` `iSup_union` `disjoint_biSup` `Finset.iSup_insert` `disjoint_comm` `sup_comm` `disjoint_sup_right_of_disjoint_sup_right` `Set.Finite.coe_toFinset`
`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`
`le_iff_eq_of_iSup_eq_top` 📖	mathematical	`iSupIndep` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`Disjoint.mono_left` `iSup₂_mono` `Disjoint.symm` `codisjoint_iff` `iSup_split_single` `le_iff_eq_of_codisjoint_of_disjoint` `le_of_eq`
`map_orderIso` 📖	mathematical	`iSupIndep`	`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`
`mem_of_biSup_eq_top` 📖	mathematical	`iSupIndep` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set` `Set.instMembership` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Set` `Set.instMembership`	—	`Disjoint.mono_right` `biSup_mono`
`mono` 📖	mathematical	`iSupIndep` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`iSupIndep`	—	`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`	`iSupIndep` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `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_comp_coe_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` 📖	mathematical	`sSupIndep` `Set` `Set.instHasSubset`	`sSupIndep`	—	`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