instCompleteLattice — Mathlib

English

A Sublattice lattice is a subsingleton iff α is empty.

Русский

Подрешетка множества является одиночной тогда и только тогда, когда множество пусто.

LaTeX

$$Subsingleton (Sublattice α) ↔ IsEmpty α$$

Lean4

/-- Sublattices of a lattice form a complete lattice. -/
instance instCompleteLattice : CompleteLattice (Sublattice α)
    where
  bot := ⊥
  bot_le := fun _S _a ↦ False.elim
  top := ⊤
  le_top := fun _S a _ha ↦ mem_top a
  inf := (· ⊓ ·)
  le_inf := fun _L _M _N hM hN _a ha ↦ ⟨hM ha, hN ha⟩
  inf_le_left := fun _L _M _a ↦ And.left
  inf_le_right := fun _L _M _a ↦ And.right
  __ := completeLatticeOfInf (Sublattice α) fun _s ↦ IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf

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