ssubset_iff_subset_not_subset

Mathlib.Order.RelClasses

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

English

a ⊂ b iff a ⊆ b and not (b ⊆ a).

Русский

a ⊂ b эквивалентно a ⊆ b и не (b ⊆ a).

LaTeX

$$$a \subset b \iff (a \subseteq b \land \neg (b \subseteq a))$$$

Lean4

theorem ssubset_iff_subset_not_subset : a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a :=
  right_iff_left_not_left

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

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

Разделы

Аффилиация

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