maximal_iff_eq — Mathlib

English

If hy: P y and hP: ∀ ⦃x⦄, P x → x ≤ y, then Maximal P x holds if and only if x = y.

Русский

Если P(y) выполняется и для любого x, если P(x), то x ≤ y, тогда Maximal P x выполняется тогда и только тогда, когда x = y.

LaTeX

$$$$ (hy : P y) \\to (\\forall x, P x \\to x \\le y) \\;\\Rightarrow\\; (Maximal P x \\iff x = y). $$$$

Lean4

/-- If `P y` holds, and everything satisfying `P` is below `y`, then `y` is the unique maximal
element satisfying `P`. -/
theorem maximal_iff_eq (hy : P y) (hP : ∀ ⦃x⦄, P x → x ≤ y) : Maximal P x ↔ x = y :=
  minimal_iff_eq (α := αᵒᵈ) hy hP

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