not_maximal_subset_iff

Mathlib.Order.Minimal

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

English

If hs: P s, then not Maximal P s is equivalent to there exists t with s ⊂ t and P t.

Русский

Если hs: P s, то не-Maximal P s эквивалентно существованию t, такого что s ⊂ t и P t.

LaTeX

$$$$ (hs : P s) \\Rightarrow (\\neg Maximal P s \\iff \\exists t\\,(s \\subset t \\land P t)). $$$$

Lean4

theorem not_maximal_subset_iff (hs : P s) : ¬Maximal P s ↔ ∃ t, s ⊂ t ∧ P t :=
  not_maximal_iff_exists_gt hs

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

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

Разделы

Аффилиация

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