instCompleteLatticeSubalgebra — Mathlib

English

There is a canonical complete lattice structure on Subalgebra R A, induced by the corresponding Galois connection with Set via gi.

Русский

Существует каноническая полная решетка на Subalgebra R A, индуцированная соответствующей Галуа-связью с множеством через gi.

LaTeX

$$$\text{CompleteLattice}(\mathrm{Subalgebra}\; R\; A)$$$

Lean4

instance : CompleteLattice (Subalgebra R A)
    where
  __ := GaloisInsertion.liftCompleteLattice Algebra.gi
  bot := (Algebra.ofId R A).range
  bot_le _S := fun _a ⟨_r, hr⟩ => hr ▸ algebraMap_mem _ _

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