subset_of_ssubset

Mathlib.Order.RelClasses

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

English

If a ⊂ b, then a ⊆ b.

Русский

Если a ⊂ b, то a ⊆ b.

LaTeX

$$$a \subset b \to a \subseteq b$$$

Lean4

theorem subset_of_ssubset (h : a ⊂ b) : a ⊆ b :=
  (ssubset_iff_subset_not_subset.1 h).1

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

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

Разделы

Аффилиация

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