instCompleteLatticeNonUnitalSubalgebra

English

The set of all NonUnitalSubalgebra R A forms a complete lattice, obtained via the Galois insertion with adjoin.

Русский

Множество всех NonUnitalSubalgebra R A образует полную решётку, полученную через Галуа-вставку с adjoin.

LaTeX

$$$\text{NonUnitalSubalgebra}(R,A) \text{ is a CompleteLattice}$$$

Lean4

instance : CompleteLattice (NonUnitalSubalgebra R A) :=
  GaloisInsertion.liftCompleteLattice NonUnitalAlgebra.gi

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