maximal_subset_iff'

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#maximal_subset_iff'

English

Maximal P s is equivalent to P s and ∀ t, P t → s ⊆ t → t ⊆ s.

Русский

Maximal P s эквивалентно P s и ∀ t, P t → s ⊆ t → t ⊆ s.

LaTeX

$$$$ Maximal P s \\iff P s \\land \\forall t\\,(P t \\to s \\subseteq t \\to t \\subseteq s). $$$$

Lean4

theorem maximal_subset_iff' : Maximal P s ↔ P s ∧ ∀ ⦃t⦄, P t → s ⊆ t → t ⊆ s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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