Theorems · Theorem · order theory
iSupIndep.comp
∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι},
iSupIndep t → Function.Injective f → iSupIndep (t ∘ f)Composing an independent indexed family with an injective function on the index results in another independent indexed family.
- Defined in
- Mathlib.Order.SupIndep
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LE.le.transproof · cited by 3,151
- iSupproof · cited by 2,415
- CompleteLatticestatement and proof · cited by 1,048
- iSupIndepstatement and proof · cited by 100
- Disjoint.mono_rightproof · cited by 64
- iSup_monoproof · cited by 37
- iSup_comp_leproof · cited by 4
- iSup_const_monoproof · cited by 3
Cited by6
Results whose statement or proof uses this declaration.
- iSupIndep.supIndep'proof · cited by 4
- Module.End.eigenvectors_linearIndependent'proof · cited by 1
- LieModule.exists_forall_mem_corootSpace_smul_add_eq_zeroproof · cited by 1
- iSupIndep.subtype_ne_bot_le_rankproof · cited by 1
- LieModule.iSupIndep_genWeightSpace'proof · cited by 1
- iSupIndep_ne_botproof · cited by 0