not_minimal_subset_iff

Mathlib.Order.Minimal

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

English

If hs: P s, then ¬Minimal P s is equivalent to ∃ t, t ⊂ s ∧ P t.

Русский

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

LaTeX

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

Lean4

theorem not_minimal_subset_iff (hs : P s) : ¬Minimal P s ↔ ∃ t, t ⊂ s ∧ P t :=
  not_minimal_iff_exists_lt hs

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

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

Разделы

Аффилиация

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