liftLattice — Mathlib

English

If α is a lattice and gi is a Galois insertion, then β inherits a lattice structure by transporting joins and meets via l and u.

Русский

Если α — решетка и существует Гalois-вставка, то β получает структуру решётки, переносом операций объединения и пересечения через l и u.

LaTeX

$$$$ \text{If } [Lattice\;α] \text{ and } (l,u) \text{ form a Galois insertion, then } \beta \text{ can be endowed with a lattice structure by transporting } \lor, \land \text{ via } l, u. $$$$

Lean4

/-- Lift the suprema and infima along a Galois insertion -/
abbrev liftLattice [Lattice α] (gi : GaloisInsertion l u) : Lattice β :=
  { gi.liftSemilatticeSup, gi.liftSemilatticeInf with }
    -- See note [reducible non-instances]

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