toDual_min' — Mathlib

English

In the dual order, the minimum corresponds to the maximum, and vice versa via image.

Русский

В двойственном порядке минимум соответствует максимуму, и обратное через образ.

LaTeX

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

Lean4

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

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