English
Let s be a subset of α. An element x ∈ α is a minimal element of s (with respect to ≤) if x ∈ s and, for every y ∈ α with y ∈ s, y ≤ x implies y = x. In words, there is no smaller element of s than x.
Русский
Пусть s ⊆ α. Элемент x ∈ α является минимальным элементом s (относительно ≤), если x ∈ s и для любого y ∈ α, если y ∈ s и y ≤ x, то y = x. Иными словами, в s нет элемента, меньшего x.
LaTeX
$$$$ Minimal (\\cdot \\in s)\, x \\Longleftrightarrow x \\in s \\land \\forall y\\,(y \\in s \\to y \\le x \\to x = y). $$$$
Lean4
theorem minimal_mem_iff {s : Set α} : Minimal (· ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y⦄, y ∈ s → y ≤ x → x = y :=
minimal_iff
