ssubset_iff_subset_ne

Mathlib.Order.RelClasses

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

English

A ⊊ B if and only if A ⊆ B and A ≠ B.

Русский

A ⊊ B тогда и только тогда, когда A ⊆ B и A ≠ B.

LaTeX

$$$ A \\subset B \\iff (A \\subseteq B) \\land (A \\neq B) $$$

Lean4

theorem ssubset_iff_subset_ne [IsAntisymm α (· ⊆ ·)] : a ⊂ b ↔ a ⊆ b ∧ a ≠ b :=
  ⟨fun h => ⟨h.subset, h.ne⟩, fun h => h.1.ssubset_of_ne h.2⟩

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

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

Разделы

Аффилиация

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