ofDual_min' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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