minimal_mem_iff — Mathlib

English

If s is Subsingleton, Minimal (· ∈ s) x holds exactly when x ∈ s.

Русский

Если s — пододнозначное множество, то минимум по принадлежности равен x ∈ s.

LaTeX

$$$\\forall x,\\; (s\\text{ subsingleton}) \\Rightarrow (\\text{Minimal}(\\cdot \\in s)\\, x) \\iff x \\in s$$$

Lean4

theorem minimal_mem_iff (h : s.Subsingleton) : Minimal (· ∈ s) x ↔ x ∈ s := by
  obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp

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