ofDual_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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