ofDual_min — Mathlib

English

In the dual order, the meet corresponds to the join under the ofDual map: ofDual (min a b) = max (ofDual a) (ofDual b).

Русский

В двойственном порядке пересечение соответствует объединению через отображение ofDual: ofDual(min a b) = max(ofDual a, ofDual b).

LaTeX

$$$ ofDual(\min a b) = \max (ofDual a) (ofDual b) $$$

Lean4

@[simp]
theorem ofDual_min (a b : αᵒᵈ) : ofDual (min a b) = max (ofDual a) (ofDual b) :=
  rfl

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