ssubset_of_subset_of_ne

Mathlib.Order.RelClasses

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

English

Let A ⊆ B and A ≠ B. Then A ⊊ B.

Русский

Пусть A ⊆ B и A ≠ B. Тогда A ⊊ B.

LaTeX

$$(A \\subseteq B) ∧ (A \\neq B) ⇒ A ⊂ B$$

Lean4

theorem ssubset_of_subset_of_ne [IsAntisymm α (· ⊆ ·)] (h₁ : a ⊆ b) (h₂ : a ≠ b) : a ⊂ b :=
  h₁.ssubset_of_not_subset <| mt h₁.antisymm h₂

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

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

Разделы

Аффилиация

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