Results on order homomorphism classes and lattice operations #
theorem
Finite.iSup_eq_iSup_subtype
{ι : Type u_1}
{K : Type u_2}
{M : Type u_3}
{F : Type u_4}
[Finite ι]
[Zero K]
[Zero M]
[ConditionallyCompleteLattice M]
[FunLike F K M]
[ZeroHomClass F K M]
[NonnegHomClass F K M]
{x : ι → K}
(hx : x ≠ 0)
{v : F}
: