minimal_true_subtype — Mathlib

English

For x in a subtype P, minimality with respect to True is equivalent to minimality of P on x.

Русский

Для x из подтипа P минимальность относительно True эквивалентна минимальности P на x.

LaTeX

$$$\\text{Minimal}(\\lambda _ : \\mathrm{True}, x) \\leftrightarrow \\text{Minimal}(P, x)$$$

Lean4

theorem minimal_true_subtype {x : Subtype P} : Minimal (fun _ ↦ True) x ↔ Minimal P x :=
  by
  obtain ⟨x, hx⟩ := x
  simp [Minimal, hx]

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