maximal_iff_isMax — Mathlib

English

If P is up-closed, then Maximal P x holds exactly when P x and IsMax x hold.

Русский

Если P является верхнезамкнутым, то Maximal P x выполняется тогда и только тогда, когда P x и IsMax x верны.

LaTeX

$$$\\text{Maximal}(P, x) \\iff P(x) \\land \\text{IsMax } x$ (при условии, что P ↑замкнуто)$$

Lean4

/-- If `P` is up-closed, then maximal elements satisfying `P` are exactly the globally maximal
elements satisfying `P`. -/
theorem maximal_iff_isMax (hP : ∀ ⦃x y⦄, P y → y ≤ x → P x) : Maximal P x ↔ P x ∧ IsMax x :=
  ⟨fun h ↦ ⟨h.prop, fun _ h' ↦ h.le_of_ge (hP h.prop h') h'⟩, fun h ↦ ⟨h.1, fun _ _ h' ↦ h.2 h'⟩⟩

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