eq_of_subset

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#Minimal.eq_of_subset

English

In the Minimal namespace, for P : Set α → Prop, s, t ⊆ α, Minimal P s and P t and t ⊆ s imply t = s.

Русский

В пространстве Minimal, для P : Set α → Prop, s, t ⊆ α, Minimal P s и P t и t ⊆ s тогда дают t = s.

LaTeX

$$$$ \\text{Minimal } P s \\land P t \\land t \\subseteq s \\;\\Longrightarrow\\; t = s. $$$$

Lean4

theorem eq_of_subset (h : Minimal P s) (ht : P t) (hts : t ⊆ s) : t = s :=
  h.eq_of_le ht hts

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

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

Разделы

Аффилиация

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