English
If α embeds injectively into a distributive lattice β via f preserving ⊔ and ⊓, then α is a distributive lattice.
Русский
Если существует инъективное вложение α в распределительную решетку β через f, сохраняющее ⊔ и ⊓, тогда α — распределительная решетка.
LaTeX
$$$[Max\\;α][Min\\;α][DistribLattice\\;β] (f:α\\to β) (hf_{inj}: \\mathrm{Injective}(f)) (map\\_sup: \\forall a b, f(a\\lor b)= f a\\lor f b) (map\\_inf: \\forall a b, f(a\\land b)= f a\\land f b) : \\mathrm{DistribLattice}(α)$$$
Lean4
/-- A type endowed with `⊔` and `⊓` is a `DistribLattice`, if it admits an injective map that
preserves `⊔` and `⊓` to a `DistribLattice`.
See note [reducible non-instances]. -/
protected abbrev distribLattice [Max α] [Min α] [DistribLattice β] (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) : DistribLattice α
where
__ := hf_inj.lattice f map_sup map_inf
le_sup_inf a b
c := by
change f ((a ⊔ b) ⊓ (a ⊔ c)) ≤ f (a ⊔ b ⊓ c)
rw [map_inf, map_sup, map_sup, map_sup, map_inf]
exact le_sup_inf
