exists_le_maximal — Mathlib

English

Let α be a preorder and a ∈ α. If α is finite, then p(a) implies there exists b ∈ α with a ≤ b and b is maximal with respect to p.

Русский

Пусть α — предордер и a ∈ α. Если α конечно, то из p(a) следует существование b ∈ α с a ≤ b и b максимален по отношению к p.

LaTeX

$$$p(a) \rightarrow ∃ b ∈ α,\ a ≤ b ∧ Maximal\ p\ b.$$$

Lean4

theorem exists_le_maximal (h : p a) : ∃ b, a ≤ b ∧ Maximal p b :=
  {x | p x}.toFinite.exists_le_maximal h

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