ofDual_sup — Mathlib

English

In the dual order, the supremum corresponds to the infimum under the ofDual map: ofDual(a ⊔ b) = ofDual(a) ⊓ ofDual(b).

Русский

В двойственном порядке, верхняя граница соответствует нижней через отображение ofDual: ofDual(a ⊔ b) = ofDual(a) ⊓ ofDual(b).

LaTeX

$$$ ofDual(a \sqcup b) = ofDual(a) \sqcap b$$$

Lean4

@[simp]
theorem ofDual_sup [Min α] (a b : αᵒᵈ) : ofDual (a ⊔ b) = ofDual a ⊓ ofDual b :=
  rfl

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