minimal_subset_iff'

Mathlib.Order.Minimal

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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