minimal_true — Mathlib

English

In any ordered set, an element x is minimal with respect to the always-true predicate if and only if x is a minimal element of the order.

Русский

Во всяком упорядоченном множестве элемент x минимален относительно всегда истинного предиката тогда и только тогда, когда x является минимальным элементом порядка.

LaTeX

$$$\\text{Minimal}(\\lambda _ : \\mathrm{Unit}, x) \\leftrightarrow \\mathrm{IsMin}\,x$$$

Lean4

@[simp]
theorem minimal_true : Minimal (fun _ ↦ True) x ↔ IsMin x := by simp [IsMin, Minimal]

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