map_ofDual_min — Mathlib

English

In the dual order, the minimum corresponds to the maximum; mapping by the dual equivalence interchanges min and max.

Русский

В порядке двойственного, минимум соответствует максимуму; отображение через дуальное отображение меняет min на max.

LaTeX

$$$\\text{For a finite } S \\subseteq \\alpha^{\\mathrm{op}},\\; \\mathrm{ofDual}(\\min' S) = \\max'(\\mathrm{image}(\\mathrm{ofDual}, S)).$$$

Lean4

theorem map_ofDual_min (s : Finset αᵒᵈ) : s.min.map ofDual = (s.image ofDual).max :=
  by
  rw [max_eq_sup_withBot, sup_image]
  exact congr_fun WithBot.map_id _

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