maximal_true — Mathlib

English

An element x is maximal with respect to the constant True predicate exactly when x is a maximal element of the order.

Русский

Элемент x максимален относительно константного истинного предиката тогда и только тогда, когда он максимальный элемент порядка.

LaTeX

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

Lean4

@[simp]
theorem maximal_true : Maximal (fun _ ↦ True) x ↔ IsMax x :=
  minimal_true (α := αᵒᵈ)

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