minimal_iff_isMin — Mathlib

English

If P is down-closed, then Minimal P x is equivalent to P x and IsMin x.

Русский

Если P является пониженно замкнуто, то Minimal P x эквивалентно P x и IsMin x.

LaTeX

$$$\\text{Minimal}(P, x) \\iff P(x) \\land \\text{IsMin } x$ (при условии, что P является снизу замкнутым)$$

Lean4

/-- If `P` is down-closed, then minimal elements satisfying `P` are exactly the globally minimal
elements satisfying `P`. -/
theorem minimal_iff_isMin (hP : ∀ ⦃x y⦄, P y → x ≤ y → P x) : Minimal P x ↔ P x ∧ IsMin x :=
  ⟨fun h ↦ ⟨h.prop, fun _ h' ↦ h.le_of_le (hP h.prop h') h'⟩, fun h ↦ ⟨h.1, fun _ _ h' ↦ h.2 h'⟩⟩

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