not_subset_of_ssubset

Mathlib.Order.RelClasses

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

English

If a ⊂ b, then not (b ⊆ a).

Русский

Если a ⊂ b, то не (b ⊆ a).

LaTeX

$$$a \subset b \to \neg (b \subseteq a)$$$

Lean4

theorem not_subset_of_ssubset (h : a ⊂ b) : ¬b ⊆ a :=
  (ssubset_iff_subset_not_subset.1 h).2

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

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

Разделы

Аффилиация

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