Basic

📁 Source: Mathlib/Data/Set/Pairwise/Basic.lean

Statistics

Metric	Count
Definitions `PairwiseDisjoint`	1
Theorems `disjoint_extend_bot`, `pairwiseDisjoint`, `range_pairwise`, `set_of_subtype`, `pairwiseDisjoint_image`, `pairwise_image`, `pairwise_ne`, `pairwise_eq_iff_exists_eq`, `pairwise_iff_exists_forall`, `image`, `insert`, `insert_of_notMem`, `insert_of_symmetric`, `mono`, `mono'`, `of_refl`, `subsingleton`, `subtype`, `elim`, `elim'`, `elim_set`, `eq_of_le`, `eq_or_disjoint`, `image_of_le`, `insert`, `insert_of_notMem`, `mono`, `mono_on`, `prod`, `range`, `subset`, `union`, `pairwise`, `exists_lt_mem_inter_of_not_pairwiseDisjoint`, `exists_ne_mem_inter_of_not_pairwiseDisjoint`, `injOn_iff_pairwise_ne`, `pairwiseDisjoint_empty`, `pairwiseDisjoint_fiber`, `pairwiseDisjoint_image_left_iff`, `pairwiseDisjoint_image_right_iff`, `pairwiseDisjoint_insert`, `pairwiseDisjoint_insert_of_notMem`, `pairwiseDisjoint_pi`, `pairwiseDisjoint_range_iff`, `pairwiseDisjoint_range_singleton`, `pairwiseDisjoint_singleton`, `pairwiseDisjoint_singleton_iff_injOn`, `pairwiseDisjoint_union`, `pairwise_bot_iff`, `pairwise_empty`, `pairwise_eq_iff_exists_eq`, `pairwise_iff_exists_forall`, `pairwise_iff_of_refl`, `pairwise_insert`, `pairwise_insert_of_notMem`, `pairwise_insert_of_symmetric`, `pairwise_insert_of_symmetric_of_notMem`, `pairwise_pair`, `pairwise_pair_of_symmetric`, `pairwise_singleton`, `pairwise_top`, `pairwise_union`, `pairwise_union_of_symmetric`, `pairwise_univ`, `pairwise_on`, `exists_lt_mem_inter_of_not_pairwise_disjoint`, `exists_ne_mem_inter_of_not_pairwise_disjoint`, `pairwise_disjoint_fiber`, `pairwise_disjoint_mono`, `pairwise_disjoint_on`, `pairwise_disjoint_on_bool`, `pairwise_ne_iff_injective`, `pairwise_not_eq_iff_injective`, `pairwise_on_bool`, `pairwise_subtype_iff_pairwise_set`, `subsingleton_setOf_mem_iff_pairwise_disjoint`	76
Total	77

Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_extend_bot` 📖	mathematical	`Pairwise` `Function.onFun` `Disjoint` `Function.FactorsThrough`	`Function.extend` `Bot.bot` `Pi.instBotForall` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`em` `Function.FactorsThrough.extend_apply` `Function.extend_apply'` `disjoint_bot_right` `disjoint_bot_left`
`pairwiseDisjoint` 📖	mathematical	`Pairwise` `Function.onFun` `Disjoint`	`Set.PairwiseDisjoint`	—	`set_pairwise`
`range_pairwise` 📖	mathematical	`Pairwise` `Function.onFun`	`Set.Pairwise` `Set.range`	—	`Set.Pairwise.image` `Set.pairwise_univ` `Set.image_univ`
`set_of_subtype` 📖	mathematical	`Pairwise` `Set.Elem` `Set` `Set.instMembership`	`Set.Pairwise`	—	`pairwise_subtype_iff_pairwise_set`

Set

Definitions

Name	Category	Theorems
`PairwiseDisjoint` 📖	MathDef	90 math math: `Finite.t2_separation`, `pairwiseDisjoint_range_iff`, `Finset.pairwiseDisjoint_singleton_iff_injOn`, `pairwiseDisjoint_pair_insert`, `Finset.product_self_eq_disjiUnion_perm_aux`, `MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff`, `Finset.pairwiseDisjoint_range_singleton`, `Finset.pairwiseDisjoint_coe`, `AddAction.orbit.pairwiseDisjoint`, `Topology.RelCWComplex.pairwiseDisjoint'`, `OrderedFinpartition.disjoint`, `exists_dist_slope_lt_pairwiseDisjoint_hasSum`, `Finpartition.disjoint`, `Besicovitch.exist_disjoint_covering_families`, `sSupIndep.pairwiseDisjoint`, `MeasureTheory.IsSetSemiring.disjointOfUnion_props`, `Partition.pairwiseDisjoint`, `Subgroup.leftCoset_cover_filter_FiniteIndex_aux`, `pairwiseDisjoint_insert_of_notMem`, `Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq`, `Finset.pairwiseDisjoint_smul_iff`, `pairwiseDisjoint_filter`, `Finset.supIndep_iff_pairwiseDisjoint`, `Besicovitch.exist_finset_disjoint_balls_large_measure`, `MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq`, `Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux`, `AddAction.IsBlock.pairwiseDisjoint_range_vadd`, `Setoid.eqv_classes_disjoint`, `pairwiseDisjoint_sUnion`, `Finset.pairwiseDisjoint_iff`, `pairwiseDisjoint_prod_left`, `IsChain.pairwiseDisjoint_iUnion₂`, `IsChain.pairwiseDisjoint_sUnion`, `Topology.CWComplex.pairwiseDisjoint'`, `MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem`, `Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall`, `MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion`, `pairwiseDisjoint_empty`, `MeasureTheory.IsSetSemiring.diff_eq_sUnion'`, `Finset.pairwiseDisjoint_map_sigmaMk`, `Subgroup.IsComplement.pairwiseDisjoint_smul`, `Finset.intervalGapsWithin_pairwiseDisjoint_Ioc`, `SimpleGraph.EdgeLabeling.pairwiseDisjoint_univ_labelGraph`, `pairwiseDisjoint_nhds`, `VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae`, `VitaliFamily.covering`, `Vitali.exists_disjoint_subfamily_covering_enlargement`, `InjOn.pairwiseDisjoint_image`, `AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq`, `AddAction.isBlock_iff_pairwiseDisjoint_range_vadd`, `Vitali.exists_disjoint_covering_ae`, `Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding`, `Besicovitch.exists_disjoint_closedBall_covering_ae`, `AddSubgroup.IsComplement.pairwiseDisjoint_vadd`, `List.pairwiseDisjoint_consFixedLengthDigits`, `Finset.pairwiseDisjoint_vadd_iff`, `MulAction.orbit.pairwiseDisjoint`, `RootedTree.subtrees_disjoint`, `pairwiseDisjoint_range_singleton`, `Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one`, `pairwiseDisjoint_vadd_iff`, `List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint`, `Finset.SupIndep.pairwiseDisjoint`, `MulAction.IsBlock.pairwiseDisjoint_range_smul`, `MulAction.isBlock_iff_pairwiseDisjoint_range_smul`, `MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion`, `pairwiseDisjoint_insert`, `pairwiseDisjoint_iff`, `pairwiseDisjoint_fiber`, `AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux`, `pairwiseDisjoint_image_right_iff`, `MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff`, `Setoid.IsPartition.pairwiseDisjoint`, `sSupIndep_iff_pairwiseDisjoint`, `pairwiseDisjoint_smul_iff`, `RealRMK.range_cut_partition`, `pairwiseDisjoint_image_left_iff`, `Besicovitch.exists_disjoint_closedBall_covering_ae_aux`, `Topology.RelCWComplex.pairwiseDisjoint`, `pairwiseDisjoint_union`, `pairwiseDisjoint_iUnion`, `VitaliFamily.FineSubfamilyOn.covering_disjoint`, `Finset.pairwiseDisjoint_pair_insert`, `pairwiseDisjoint_singleton`, `Pairwise.pairwiseDisjoint`, `Finset.pairwiseDisjoint_slice`, `Vitali.exists_disjoint_covering_ae'`, `AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero`, `MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion`, `pairwiseDisjoint_singleton_iff_injOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt_mem_inter_of_not_pairwiseDisjoint` 📖	mathematical	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instInter`	—	`exists_ne_mem_inter_of_not_pairwiseDisjoint` `lt_or_lt_iff_ne`
`exists_ne_mem_inter_of_not_pairwiseDisjoint` 📖	mathematical	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`instMembership` `instInter`	—	`nonempty_iff_ne_empty` `bot_eq_empty` `le_bot_iff`
`injOn_iff_pairwise_ne` 📖	mathematical	—	`InjOn` `Pairwise`	—	—
`pairwiseDisjoint_empty` 📖	mathematical	—	`PairwiseDisjoint` `Set` `instEmptyCollection`	—	`pairwise_empty`
`pairwiseDisjoint_fiber` 📖	mathematical	—	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `preimage` `instSingletonSet`	—	`disjoint_iff_inf_le`
`pairwiseDisjoint_image_left_iff` 📖	mathematical	—	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `image` `InjOn` `SProd.sprod` `instSProd`	—	`PairwiseDisjoint.elim` `not_disjoint_iff` `mem_image_of_mem` `disjoint_iff_inf_le` `mk_mem_prod`
`pairwiseDisjoint_image_right_iff` 📖	mathematical	—	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `image` `InjOn` `SProd.sprod` `instSProd`	—	`PairwiseDisjoint.elim` `not_disjoint_iff` `mem_image_of_mem` `disjoint_iff_inf_le` `mk_mem_prod`
`pairwiseDisjoint_insert` 📖	mathematical	—	`PairwiseDisjoint` `Set` `instInsert` `Disjoint`	—	`pairwise_insert_of_symmetric` `Symmetric.comap` `symmetric_disjoint`
`pairwiseDisjoint_insert_of_notMem` 📖	mathematical	`Set` `instMembership`	`PairwiseDisjoint` `instInsert` `Disjoint`	—	`pairwise_insert_of_symmetric_of_notMem` `Symmetric.comap` `symmetric_disjoint`
`pairwiseDisjoint_pi` 📖	mathematical	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`pi` `univ`	—	`disjoint_left` `PairwiseDisjoint.elim_set`
`pairwiseDisjoint_range_iff` 📖	mathematical	—	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `range` `Disjoint`	—	—
`pairwiseDisjoint_range_singleton` 📖	mathematical	—	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `range` `instSingletonSet`	—	`Pairwise.range_pairwise` `disjoint_singleton`
`pairwiseDisjoint_singleton` 📖	mathematical	—	`PairwiseDisjoint` `Set` `instSingletonSet`	—	`pairwise_singleton`
`pairwiseDisjoint_singleton_iff_injOn` 📖	mathematical	—	`PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `instSingletonSet` `InjOn`	—	—
`pairwiseDisjoint_union` 📖	mathematical	—	`PairwiseDisjoint` `Set` `instUnion` `Disjoint`	—	`pairwise_union_of_symmetric` `Symmetric.comap` `symmetric_disjoint`
`pairwise_bot_iff` 📖	mathematical	—	`Pairwise` `Bot.bot` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra` `Subsingleton`	—	`Pairwise.eq` `Subsingleton.pairwise`
`pairwise_empty` 📖	mathematical	—	`Pairwise` `Set` `instEmptyCollection`	—	`Subsingleton.pairwise` `subsingleton_empty`
`pairwise_eq_iff_exists_eq` 📖	mathematical	—	`Pairwise`	—	`pairwise_iff_exists_forall` `eq_isEquiv`
`pairwise_iff_exists_forall` 📖	mathematical	—	`Pairwise` `Function.onFun`	—	`eq_empty_or_nonempty` `instIsEmptyFalse` `Nonempty.pairwise_iff_exists_forall`
`pairwise_iff_of_refl` 📖	mathematical	—	`Pairwise`	—	`of_eq`
`pairwise_insert` 📖	mathematical	—	`Pairwise` `Set` `instInsert`	—	—
`pairwise_insert_of_notMem` 📖	mathematical	`Set` `instMembership`	`Pairwise` `instInsert`	—	`pairwise_insert`
`pairwise_insert_of_symmetric` 📖	mathematical	`Symmetric`	`Pairwise` `Set` `instInsert`	—	`Symmetric.iff`
`pairwise_insert_of_symmetric_of_notMem` 📖	mathematical	`Symmetric` `Set` `instMembership`	`Pairwise` `instInsert`	—	`pairwise_insert_of_notMem` `Symmetric.iff`
`pairwise_pair` 📖	mathematical	—	`Pairwise` `Set` `instInsert` `instSingletonSet`	—	—
`pairwise_pair_of_symmetric` 📖	mathematical	`Symmetric`	`Pairwise` `Set` `instInsert` `instSingletonSet`	—	`pairwise_insert_of_symmetric`
`pairwise_singleton` 📖	mathematical	—	`Pairwise` `Set` `instSingletonSet`	—	`Subsingleton.pairwise` `subsingleton_singleton`
`pairwise_top` 📖	mathematical	—	`Pairwise` `Top.top` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`pairwise_of_forall`
`pairwise_union` 📖	mathematical	—	`Pairwise` `Set` `instUnion`	—	—
`pairwise_union_of_symmetric` 📖	mathematical	`Symmetric`	`Pairwise` `Set` `instUnion`	—	`pairwise_union` `Symmetric.iff`
`pairwise_univ` 📖	mathematical	—	`Pairwise` `univ` `Pairwise`	—	—

Set.InjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwiseDisjoint_image` 📖	mathematical	`Set.InjOn`	`Set.PairwiseDisjoint` `Set.image`	—	`pairwise_image`
`pairwise_image` 📖	mathematical	`Set.InjOn`	`Set.Pairwise` `Set.image` `Function.onFun`	—	`eq_iff`
`pairwise_ne` 📖	mathematical	`Set.InjOn`	`Set.Pairwise`	—	`Set.injOn_iff_pairwise_ne`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwise_eq_iff_exists_eq` 📖	mathematical	`Set.Nonempty`	`Set.Pairwise`	—	`pairwise_iff_exists_forall` `eq_isEquiv`
`pairwise_iff_exists_forall` 📖	mathematical	`Set.Nonempty`	`Set.Pairwise` `Function.onFun`	—	`eq_or_ne` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `IsTrans.trans` `IsPreorder.toIsTrans` `symm` `IsEquiv.toSymm`

Set.Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`Set.Pairwise` `Function.onFun`	`Set.image`	—	`Set.forall_mem_image`
`insert` 📖	mathematical	`Set.Pairwise`	`Set` `Set.instInsert`	—	`Set.pairwise_insert`
`insert_of_notMem` 📖	mathematical	`Set` `Set.instMembership` `Set.Pairwise`	`Set.instInsert`	—	`Set.pairwise_insert_of_notMem`
`insert_of_symmetric` 📖	mathematical	`Set.Pairwise` `Symmetric`	`Set` `Set.instInsert`	—	`Set.pairwise_insert_of_symmetric`
`mono` 📖	—	`Set` `Set.instHasSubset` `Set.Pairwise`	—	—	—
`mono'` 📖	—	`Pi.hasLe` `Prop.le` `Set.Pairwise`	—	—	`imp`
`of_refl` 📖	—	`Set.Pairwise` `Set` `Set.instMembership`	—	—	`Set.pairwise_iff_of_refl`
`subsingleton` 📖	mathematical	`Set.Pairwise` `Bot.bot` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra`	`Set.Subsingleton`	—	`Set.pairwise_bot_iff`
`subtype` 📖	mathematical	`Set.Pairwise`	`Pairwise` `Set.Elem` `Set` `Set.instMembership`	—	`pairwise_subtype_iff_pairwise_set`

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim` 📖	—	`Set.PairwiseDisjoint` `Set` `Set.instMembership` `Disjoint`	—	—	`Set.Pairwise.eq`
`elim'` 📖	—	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Set` `Set.instMembership`	—	—	`elim` `Disjoint.eq_bot`
`elim_set` 📖	—	`Set.PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set.instMembership`	—	—	`elim` `Set.not_disjoint_iff`
`eq_of_le` 📖	—	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`elim'` `inf_of_le_left`
`eq_or_disjoint` 📖	mathematical	`Set.PairwiseDisjoint` `Set` `Set.instMembership`	`Disjoint`	—	`elim`
`image_of_le` 📖	mathematical	`Set.PairwiseDisjoint` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder`	`Set.image`	—	`Disjoint.mono`
`insert` 📖	mathematical	`Set.PairwiseDisjoint` `Disjoint`	`Set` `Set.instInsert`	—	`Set.pairwiseDisjoint_insert`
`insert_of_notMem` 📖	mathematical	`Set.PairwiseDisjoint` `Set` `Set.instMembership` `Disjoint`	`Set.instInsert`	—	`Set.pairwiseDisjoint_insert_of_notMem`
`mono` 📖	—	`Set.PairwiseDisjoint` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`mono_on`
`mono_on` 📖	—	`Set.PairwiseDisjoint` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`Disjoint.mono`
`prod` 📖	mathematical	`Set.PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`SProd.sprod` `Set.instSProd`	—	`Set.disjoint_left` `elim_set`
`range` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.PairwiseDisjoint`	`Set.range` `Set.Elem`	—	`Disjoint.mono`
`subset` 📖	—	`Set.PairwiseDisjoint` `Set` `Set.instHasSubset`	—	—	`Set.Pairwise.mono`
`union` 📖	mathematical	`Set.PairwiseDisjoint` `Disjoint`	`Set` `Set.instUnion`	—	`Set.pairwiseDisjoint_union`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwise` 📖	mathematical	`Set.Subsingleton`	`Set.Pairwise`	—	—

Symmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwise_on` 📖	mathematical	`Symmetric`	`Pairwise` `Function.onFun`	—	`LT.lt.ne` `Ne.lt_or_gt`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt_mem_inter_of_not_pairwise_disjoint` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Preorder.toLT` `PartialOrder.toPreorder` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.instMembership` `Set.instInter`	—	`Set.exists_lt_mem_inter_of_not_pairwiseDisjoint` `Set.pairwise_univ`
`exists_ne_mem_inter_of_not_pairwise_disjoint` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Set.instMembership` `Set.instInter`	—	`Set.exists_ne_mem_inter_of_not_pairwiseDisjoint` `Set.pairwise_univ`
`pairwise_disjoint_fiber` 📖	mathematical	—	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set.preimage` `Set.instSingletonSet`	—	`Set.pairwise_univ` `Set.pairwiseDisjoint_fiber`
`pairwise_disjoint_mono` 📖	—	`Pairwise` `Function.onFun` `Disjoint` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`Pairwise.mono` `Disjoint.mono`
`pairwise_disjoint_on` 📖	mathematical	—	`Pairwise` `Function.onFun` `Disjoint`	—	`Symmetric.pairwise_on` `Disjoint.symm`
`pairwise_disjoint_on_bool` 📖	mathematical	—	`Pairwise` `Function.onFun` `Disjoint`	—	`pairwise_on_bool` `Disjoint.symm`
`pairwise_ne_iff_injective` 📖	mathematical	—	`Pairwise`	—	—
`pairwise_not_eq_iff_injective` 📖	mathematical	—	`Pairwise`	—	—
`pairwise_on_bool` 📖	mathematical	`Symmetric`	`Pairwise` `Function.onFun`	—	`instIsEmptyFalse`
`pairwise_subtype_iff_pairwise_set` 📖	mathematical	—	`Pairwise` `Set.Elem` `Set` `Set.instMembership` `Set.Pairwise`	—	—
`subsingleton_setOf_mem_iff_pairwise_disjoint` 📖	mathematical	—	`Set.Subsingleton` `setOf` `Set` `Set.instMembership` `Pairwise` `Function.onFun` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	—	`Set.disjoint_left` `by_contra`

---

← Back to Index