ssubset_of_subset_not_subset

Mathlib.Order.RelClasses

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

English

Let A and B be sets with A ⊆ B. If B is not a subset of A, then A ⊊ B.

Русский

Пусть A и B — множества, такие что A ⊆ B. Если B ⊄ A, то A ⊊ B.

LaTeX

$$$ (A \\subseteq B) \\land (B \\nsubseteq A) \\Rightarrow A \\subsetneq B $$$

Lean4

theorem ssubset_of_subset_not_subset (h₁ : a ⊆ b) (h₂ : ¬b ⊆ a) : a ⊂ b :=
  ssubset_iff_subset_not_subset.2 ⟨h₁, h₂⟩

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

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

Разделы

Аффилиация

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