eq_of_subset_of_not_ssubset

Mathlib.Order.RelClasses

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

English

If A ⊆ B and not (A ⊊ B), then A = B.

Русский

Если A ⊆ B и не A ⊊ B, то A = B.

LaTeX

$$(A \\subseteq B) ∧ ¬ (A \\subset B) ⇒ A = B$$

Lean4

theorem eq_of_subset_of_not_ssubset [IsAntisymm α (· ⊆ ·)] (hab : a ⊆ b) (hba : ¬a ⊂ b) : a = b :=
  (eq_or_ssubset_of_subset hab).resolve_right hba

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

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

Разделы

Аффилиация

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