instSupCoe — Mathlib

English

A sublattice inherits a supremum operation from the ambient lattice: for a,b ∈ L, max_L(a,b) = ⟨a ⊔ b, L.supClosed a.2 b.2⟩.

Русский

Подрешетка наследует операцию наибольшего из окружающей решетки: для a,b ∈ L, максимум в подрешетке равен ⟨a ⊔ b, L.supClosed a.2 b.2⟩.

LaTeX

$$$ \\max_L(a,b) = \\langle a \\lor b, L.supClosed(a.2,b.2) \\rangle $$$

Lean4

/-- A sublattice of a lattice inherits a supremum. -/
instance instSupCoe : Max L where max a b := ⟨a ⊔ b, L.supClosed a.2 b.2⟩

Похожие утверждения