ofIsSublattice — Mathlib

English

Membership in the sublattice defined by a set s with SupClosed and InfClosed is equivalent to membership in s.

Русский

Членство в под-области, заданной множеством s со свойствами supClosed и infClosed, эквивалентно членству в s.

LaTeX

$$$a \in \operatorname{mk}(s, h_{\mathrm{sup}}, h_{\mathrm{inf}}) \iff a \in s$$$

Lean4

/-- Turn a set closed under supremum and infimum into a sublattice. -/
abbrev ofIsSublattice (s : Set α) (hs : IsSublattice s) : Sublattice α :=
  ⟨s, hs.1, hs.2⟩

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