English
Suppose hy: P(y) and hP: ∀ ⦃x⦄, P(x) → y ≤ x. Then Minimal P x holds if and only if x = y; i.e., y is the unique minimal element with property P.
Русский
Пусть hy: P(y) и hP: ∀ x, P(x) → y ≤ x. Тогда Minimal P x эквивалентно x = y; то есть y — единственный минимальный элемент, удовлетворяющий P.
LaTeX
$$$$ (hy : P y) \\land (\\forall x, P x \\to y \\le x) \\;\\Rightarrow\\; (Minimal P x \\iff x = y). $$$$
Lean4
/-- If `P y` holds, and everything satisfying `P` is above `y`, then `y` is the unique minimal
element satisfying `P`. -/
theorem minimal_iff_eq (hy : P y) (hP : ∀ ⦃x⦄, P x → y ≤ x) : Minimal P x ↔ x = y :=
⟨fun h ↦ h.eq_of_ge hy (hP h.prop), by rintro rfl; exact ⟨hy, fun z hz _ ↦ hP hz⟩⟩
