Pairwise

📁 Source: Mathlib/Logic/Pairwise.lean

Statistics

Metric	Count
Definitions Pairwise, Pairwise, Pairwise	3
Theorems pairwise_comp_iff, pairwise_ne, injective_iff_pairwise_ne, comp_of_injective, eq, mono, of_comp_of_surjective, set_pairwise, set_pairwise_iff, eq, imp, imp_on, on_injective, pairwise_of_forall, pairwise, pairwise_fin_succ_iff, pairwise_fin_succ_iff_of_isSymm	17
Total	20

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_iff_pairwise_ne 📖	mathematical	—	Pairwise onFun	—	not_imp_not

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise_comp_iff 📖	mathematical	Function.Bijective	Pairwise Function.onFun	—	Pairwise.of_comp_of_surjective surjective Pairwise.comp_of_injective injective

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise_ne 📖	mathematical	—	Pairwise Function.onFun	—	Function.injective_iff_pairwise_ne

Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_of_injective 📖	mathematical	Pairwise	Function.onFun	—	—
eq 📖	—	Pairwise	—	—	not_imp_comm
mono 📖	—	Pairwise	—	—	—
of_comp_of_surjective 📖	—	Pairwise Function.onFun	—	—	Function.Surjective.forall₂
set_pairwise 📖	mathematical	Pairwise	Set.Pairwise	—	—

Reflexive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
set_pairwise_iff 📖	mathematical	Reflexive	Set.Pairwise	—	—

Set

Definitions

Name	Category	Theorems
Pairwise 📖	MathDef	68 math math: pairwise_iUnion, InjOn.pairwise_ne, Finset.pairwise_subtype_iff_pairwise_finset, IsMulIndecomposable.pairwise_baseOf_div_notMem, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, IsMulIndecomposable.pairwise_div_notMem_range, convex_iff_pairwise_pos, Pairwise.range_pairwise, pairwise_sUnion, pairwise_empty, pairwise_univ, pairwise_of_forall, SimpleGraph.isIndepSet_iff, PairwiseDisjoint.aedisjoint, strictConvex_iff_openSegment_subset, Nonempty.pairwise_eq_iff_exists_eq, IsChain.pairwise_sUnion, pairwise_pair, Submodule.IsMinimalPrimaryDecomposition.distinct, pairwise_eq_iff_exists_eq, pairwise_insert_of_symmetric_of_notMem, Subsingleton.pairwise, intersecting_iff_pairwise_not_disjoint, BoxIntegral.Prepartition.pairwiseDisjoint, InjOn.pairwise_image, pairwise_singleton, Ideal.iSup_iInf_eq_top_iff_pairwise, pairwise_insert, List.Nodup.pairwise_coe, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, pairwise_union, pairwise_bot_iff, List.pairwise_iff_coe_toFinset_pairwise, Submodule.isPrimary_decomposition_pairwise_ne_radical, pairwise_insert_of_symmetric, Reflexive.set_pairwise_iff, pairwise_insert_of_notMem, IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime, SimpleGraph.isClique_iff, Pairwise.set_of_subtype, pairwise_pair_of_symmetric, concaveOn_iff_pairwise_pos, Finset.pairwise_subtype_iff_pairwise_finset', pairwise_union_of_symmetric, UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime, SimpleGraph.cliqueFreeOn_two, Equiv.Perm.cycleFactorsFinset_mem_commute, strictConvex_iff_div, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, pairwise_subtype_iff_pairwise_set, pairwise_iff_exists_forall, pairwise_iff_of_refl, pairwise_iUnion₂_iff, Ideal.isPrimary_decomposition_pairwise_ne_radical, injOn_iff_pairwise_ne, pairwise_top, IsAddIndecomposable.pairwise_sub_notMem_range, SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint, Pairwise.set_pairwise, List.Pairwise.set_pairwise, EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq, IsAddIndecomposable.pairwise_baseOf_sub_notMem, Nonempty.pairwise_iff_exists_forall, convexOn_iff_pairwise_pos, IsChain.pairwise_iUnion₂, IsAddIndecomposable.pairwise_sub_notMem_range', RootPairing.baseOf_pairwise_pairing_le_zero, IsMulIndecomposable.pairwise_div_notMem_range'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise_of_forall 📖	mathematical	—	Pairwise	—	—

Set.Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	—	Set.Pairwise Set Set.instMembership	—	—	of_not_not
imp 📖	—	Set.Pairwise	—	—	imp_on Set.pairwise_of_forall
imp_on 📖	—	Set.Pairwise	—	—	—
on_injective 📖	mathematical	Set.Pairwise Set Set.instMembership	Pairwise Function.onFun	—	—

Stream'.Seq

Definitions

Name	Category	Theorems
Pairwise 📖	MathDef	4 math math: Pairwise.coind, Pairwise_cons_nil, Pairwise.nil, Pairwise.coind_trans

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise 📖	mathematical	—	Pairwise	—	—

(root)

Definitions

Name	Category	Theorems
Pairwise 📖	MathDef	147 math math: Set.pairwise_disjoint_Ioc_zpow, Set.pairwise_disjoint_Ioo_add_zsmul, MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero, Function.Injective.pairwise_ne, Finset.pairwise_subtype_iff_pairwise_finset, Set.pairwise_disjoint_Ico_zsmul, Set.pairwise_disjoint_Ioo_mul_zpow, Congruent.pairwise_edist_eq, MeasureTheory.pairwise_disjoint_fundamentalInterior, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, Antitone.pairwise_disjoint_on_Ioc_pred, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, iSupIndep.pairwiseDisjoint, pairwise_disjoint_fiber, Antitone.pairwise_disjoint_on_Ioo_pred, Besicovitch.SatelliteConfig.h, SimpleGraph.ComponentCompl.pairwise_disjoint, pairwise_on_bool, congruent_iff_pairwise_edist_eq, pairwise_coprime_iff_coprime_prod, Module.DualBases.eval_of_ne, Set.pairwise_disjoint_Ioc_zsmul, Congruent.pairwise_dist_eq, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, Monotone.pairwise_disjoint_on_Ioc_pred, Antitone.pairwise_disjoint_on_Ioo_succ, Set.pairwise_disjoint_Ioo_add_intCast, Set.pairwise_disjoint_vadd_iff, t1Space_iff_exists_open, pairwise_ne_iff_injective, Finset.pairwise_cons', t0Space_iff_uniformity', Set.pairwise_disjoint_Ioc_add_zsmul, Set.pairwise_univ, exists_isClopen_of_totally_separated, exists_seq_norm_le_one_le_norm_sub, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, orthogonalIdempotents_iff, Nat.pairwise_coprime_pow_primeFactors_factorization, MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac, InnerProductSpace.gramSchmidt_pairwise_orthogonal, Orthonormal.isHilbertSum, Set.pairwise_disjoint_Ico_add_intCast, similar_iff_exists_pairwise_dist_eq, pairwise_not_eq_iff_injective, exists_sum_eq_one_iff_pairwise_coprime', SimpleGraph.EdgeLabeling.pairwise_disjoint_labelGraph, EisensteinSeries.pairwise_disjoint_gammaSet, MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac, Orthonormal.linearIsometryEquiv_symm_apply_single_one, Finset.pairwise_cons, Antitone.pairwise_disjoint_on_Ioc_succ, exists_seq_infinite_isOpen_pairwise_disjoint, Nat.pairwise_one_le_dist, congruent_iff_pairwise_nndist_eq, SimpleGraph.pairwise_disjoint_supp_connectedComponent, Set.pairwise_disjoint_Ioo_zpow, VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype, t2Space_iff_disjoint_nhds, Equiv.Perm.signAux3_mul_and_swap, similar_iff_exists_pairwise_edist_eq, Set.pairwise_disjoint_Ioc_intCast, Multiset.pairwise_disjoint_powersetCard, Equiv.Perm.pairwise_commute_of_mem_zpowers, Congruent.pairwise_nndist_eq, Set.pairwise_disjoint_Ioo_zsmul, Set.Pairwise.subtype, Pairwise.of_gt, Nat.pairwise_coprime_fermatNumber, t0Space_iff_exists_isOpen_xor'_mem, IndexedPartition.disjoint, Set.pairwise_disjoint_Ioc_add_intCast, MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one, Monotone.pairwise_disjoint_on_Ico_pred, CompleteOrthogonalIdempotents.iff_ortho_complete, Metric.frontier_thickening_disjoint, Monotone.pairwise_disjoint_on_Ioo_succ, OrthogonalIdempotents.ortho, similar_iff_exists_pairwise_nndist_eq, T2Space.t2, Symmetric.pairwise_on, t2Space_iff_nhds, Monotone.pairwise_disjoint_on_Ioo_pred, Monotone.pairwise_disjoint_on_Ioc_succ, Set.pairwise_disjoint_Ico_zpow, t0Space_iff_not_inseparable, Metric.frontier_cthickening_disjoint, Finset.pairwise_subtype_iff_pairwise_finset', Fintype.exists_disjointed_le, MeasureTheory.IsFundamentalDomain.aedisjoint, Pi.single_addCommute, Set.Pairwise.on_injective, Similar.exists_pairwise_dist_eq, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, Orthonormal.orthogonalFamily, Function.Bijective.pairwise_comp_iff, pairwise_disjoint_on_bool, Function.injective_iff_pairwise_ne, orthogonalFamily_iff_pairwise, pairwise_subtype_iff_pairwise_set, Set.pairwise_disjoint_Ico_intCast, disjoint_disjointed, subsingleton_setOf_mem_iff_pairwise_disjoint, similar_iff_exists_pos_pairwise_dist_eq, ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, Set.pairwise_disjoint_smul_iff, EquivLike.pairwise_comp_iff, t0Space_iff_or_notMem_closure, pairwise_iff_gt, Equiv.Perm.pairwise_disjoint_of_mem_zpowers, MeasureTheory.IsAddFundamentalDomain.aedisjoint, Antitone.pairwise_disjoint_on_Ico_pred, exists_sum_eq_one_iff_pairwise_coprime, pairwise_iff_lt, Similar.exists_pos_pairwise_dist_eq, pairwise_fin_succ_iff_of_isSymm, pairwise_isRelPrime_iff_isRelPrime_prod, MeasureTheory.pairwise_disjoint_addFundamentalInterior, totallySeparatedSpace_iff_exists_isClopen, pairwise_disjoint_nhds, Besicovitch.SatelliteConfig.exists_normalized, SimpleGraph.IsSRGWith.of_not_adj, Set.pairwise_disjoint_Ico_add_zsmul, pairwise_fin_succ_iff, OrthogonalFamily.pairwise, iSupIndep_iff_pairwiseDisjoint, Polynomial.pairwise_coprime_X_sub_C, Metric.uniformSpace_eq_bot, Pairwise.of_lt, Int.pairwise_one_le_dist, congruent_iff_pairwise_dist_eq, Similar.exists_pairwise_edist_eq, exists_seq_of_forall_finset_exists', exists_seq_norm_le_one_le_norm_sub', Finset.pairwise_disjoint_powersetCard, Set.pairwise_disjoint_Ioo_intCast, TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, NumberField.mixedEmbedding.disjoint_negAt_plusPart, Similar.exists_pairwise_nndist_eq, Filter.HasBasis.uniformSpace_eq_bot, Subsingleton.pairwise, pairwise_disjoint_on, Pi.mulSingle_commute, Antitone.pairwise_disjoint_on_Ico_succ, t2Space_iff, Monotone.pairwise_disjoint_on_Ico_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise_fin_succ_iff 📖	mathematical	—	Pairwise	—	Iff.not
pairwise_fin_succ_iff_of_isSymm 📖	mathematical	—	Pairwise	—	comm

---

← Back to Index