exists_maximal_ge_of_wellFoundedGT

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#exists_maximal_ge_of_wellFoundedGT

← MathLib Explorer

English

If P holds at a, there exists b ≥ a such that Maximal P b.

Русский

Если P выполняется для a, существует b ≥ a такое, что Maximal P b.

LaTeX

$$$ P a \rightarrow \exists b, a \le b \land \operatorname{Maximal} P b $$$

Lean4

theorem exists_maximal_ge_of_wellFoundedGT (P : α → Prop) (a : α) (ha : P a) : ∃ b, a ≤ b ∧ Maximal P b :=
  exists_minimal_le_of_wellFoundedLT (α := αᵒᵈ) P a ha

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru