map — Mathlib

English

A bounded lattice homomorphism preserves complementation: if a and b are complements, then f(a) and f(b) are complements.

Русский

Гомоморфизм ограниченной решетки сохраняет дополнение: если a и b комплементы, тогда f(a) и f(b) тоже комплементы.

LaTeX

$$$f: F \quad [BoundedLatticeHomClass F \alpha \beta] \; \{a,b\} \; (IsCompl\; a\; b) \Rightarrow IsCompl (f a) (f b)$$$

Lean4

theorem map [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] {a b : α} (f : F) (h : IsCompl a b) :
    IsCompl (f a) (f b) :=
  ⟨h.1.map _, h.2.map _⟩

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