English
If α maps injectively into a lattice β via f and preserves ⊔ and ⊓, then α inherits a lattice structure.
Русский
Если существует инъективное отображение f: α → β, сохраняющее ⊔ и ⊓, и β — решетка, то α наследует структуру решетки.
LaTeX
$$$[Max\\;α][Min\\;α][Lattice\\;β] \\; (f:α\\to β) \\; (hf_{inj}: \\mathrm{Injective}(f)) \\; (map\\_sup: \\forall a b, f(a\\sqcup b)= f a\\sqcup f b) \\; (map\\_inf: \\forall a b, f(a\\sqcap b)= f a\\sqcap f b) : \\mathrm{Lattice}(α)$$$
Lean4
/-- A type endowed with `⊔` and `⊓` is a `Lattice`, if it admits an injective map that
preserves `⊔` and `⊓` to a `Lattice`.
See note [reducible non-instances]. -/
protected abbrev lattice [Max α] [Min α] [Lattice β] (f : α → β) (hf_inj : Function.Injective f)
(map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : Lattice α
where
__ := hf_inj.semilatticeSup f map_sup
__ := hf_inj.semilatticeInf f map_inf
