dual — Mathlib

English

If s has least element a, then in the dual order the pair (ofDual⁻¹s, toDual a) yields the greatest element.

Русский

Если у множества s есть наименьший элемент a, то во втором порядке пара (ofDual⁻¹s, toDual a) задаёт наибольший элемент.

LaTeX

$$$$ IsLeast(s,a) \Rightarrow IsGreatest(\mathrm{ofDual}^{-1}(s), \mathrm{toDual}(a)) $$$$

Lean4

theorem dual (h : IsLeast s a) : IsGreatest (ofDual ⁻¹' s) (toDual a) :=
  h

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