coe — Mathlib

English

Turn a set closed under sup and inf into a Sublattice: if s is IsSublattice, then ofIsSublattice(s, hs) is a Sublattice.

Русский

Преобразование множества, замкнутого относительно sup и inf, в под–слабат: если s удовлетворяет IsSublattice, то ofIsSublattice(s, hs) образует Sublattice.

LaTeX

$$$\text{ofIsSublattice}(s, hs) : \text{Sublattice}(\alpha)$$$

Lean4

/-- See Note [custom simps projection]. -/
def coe (L : Sublattice α) : Set α :=
  L

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