minimal_toDual — Mathlib

English

Dual-to-minimal equivalence: Minimal (fun x => P (ofDual x)) (toDual x) ↔ Maximal P x.

Русский

Эквивалентность минимального через двойственный переход: Minimal(P(ofDual x)) (toDual x) ↔ Maximal P x.

LaTeX

$$$ \text{Minimal}(P(\mathrm{ofDual} \, x)) \mathrm{toDual}\ x \\iff \text{Maximal } P x $$$

Lean4

@[simp]
theorem minimal_toDual : Minimal (fun x ↦ P (ofDual x)) (toDual x) ↔ Maximal P x :=
  Iff.rfl

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