maximal_true_subtype — Mathlib

English

For x in a subtype P, being maximal with respect to the constant True predicate is equivalent to being maximal in P on x.

Русский

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

LaTeX

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

Lean4

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

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