Theorems · Theorem · order theory
Finset.supIndep_iff_disjoint_erase
∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
[inst_2 : DecidableEq ι], s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)The RHS looks like the definition of iSupIndep.
- Defined in
- Mathlib.Order.SupIndep
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LatticeOrderBotDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Disjointstatement and proof · cited by 2,201
- OrderBotstatement and proof · cited by 1,055
- Latticestatement and proof · cited by 916
- Finset.supstatement and proof · cited by 530
- Finset.erasestatement and proof · cited by 455
- Disjoint.mono_rightproof · cited by 64
- Finset.mem_eraseproof · cited by 61
- Finset.notMem_eraseproof · cited by 59
- Finset.SupIndepstatement and proof · cited by 52
- Finset.erase_subsetproof · cited by 31
- Finset.sup_monoproof · cited by 25
Cited by6
Results whose statement or proof uses this declaration.
- Finset.SupIndep.biUnionproof · cited by 4
- iSupIndep_comp_coe_iff_supIndepproof · cited by 3
- iSupIndep_iff_supIndepproof · cited by 2
- Submodule.inf_iSup_genEigenspaceproof · cited by 1
- LinearMap.ker_noncommProd_eq_of_supIndep_kerproof · cited by 1
- iSupIndep_iff_supIndep_of_injOnproof · cited by 0