maximal_false — Mathlib

English

There is no x for which the predicate constantly False is maximal; i.e., no element can be maximal with respect to a predicate that is always false.

Русский

Не существует элемента x, который был бы максимальным относительно предиката, равного ложному на всей области; других слов.

LaTeX

$$$\\neg \\operatorname{Maximal}(\\lambda _ : \\alpha, \\mathrm{False})\\, x$$$

Lean4

@[simp]
theorem maximal_false : ¬Maximal (fun _ ↦ False) x := by simp [Maximal]

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