Theorems · Theorem · order theory
Finite.iSup_eq_iSup_subtype
∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {F : Type u_4} [Finite ι] [inst : Zero K] [inst_1 : Zero M]
[inst_2 : ConditionallyCompleteLattice M] [inst_3 : FunLike F K M] [ZeroHomClass F K M] [NonnegHomClass F K M]
{x : ι → K}, x ≠ 0 → ∀ {v : F}, ⨆ i, v (x i) = ⨆ i, v (x ↑i)- Defined in
- Mathlib.Algebra.Order.Hom.Lattice
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finitestatement and proof · cited by 3,029
- FunLikestatement and proof · cited by 2,560
- iSupstatement and proof · cited by 2,415
- le_antisymmproof · cited by 2,068
- map_zeroproof · cited by 1,614
- le_rflproof · cited by 1,558
- eq_or_neproof · cited by 1,117
- ConditionallyCompleteLatticestatement and proof · cited by 364
- NonnegHomClass.apply_nonnegproof · cited by 79
- ZeroHomClassstatement and proof · cited by 74
- ciSup_leproof · cited by 56
Cited by1
Results whose statement or proof uses this declaration.
- NumberField.absNorm_mul_finprod_finitePlace_eq_oneproof · cited by 1