ofDual_max' — Mathlib

English

For a nonempty finite subset S of α^op, the dual of its maximum equals the minimum of the dual image.

Русский

Для непустого конечного подмножества S α^op дуальное максимума равняется минимуму дуального образа.

LaTeX

$$$\\mathrm{ofDual}(\\max' S) = \\min'(\\mathrm{image}(\\mathrm{ofDual}, S))$$$

Lean4

theorem ofDual_max' {s : Finset αᵒᵈ} (hs : s.Nonempty) : ofDual (max' s hs) = min' (s.image ofDual) (hs.image _) := by
  simp [min'_eq_inf', max'_eq_sup']

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