eq_or_ssubset_of_subset

Mathlib.Order.RelClasses

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

English

Let A ⊆ B. Then either A = B or A ⊊ B.

Русский

Пусть A ⊆ B. Тогда либо A = B, либо A ⊊ B.

LaTeX

$$$ A \\subseteq B \\Rightarrow (A = B) \\lor (A \\subset B) $$$

Lean4

theorem eq_or_ssubset_of_subset [IsAntisymm α (· ⊆ ·)] (h : a ⊆ b) : a = b ∨ a ⊂ b :=
  (em (b ⊆ a)).imp h.antisymm h.ssubset_of_not_subset

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

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

Разделы

Аффилиация

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