ssubset_of_eq_of_ssubset

Mathlib.Order.RelClasses

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

English

If a = b and b ⊆ c, then a ⊆ c (in HasSSubset context).

Русский

Если a = b и b ⊆ c, то a ⊆ c (в контексте HasSSubset).

LaTeX

$$$a = b \to b \subset c \to a \subset c$$$

Lean4

theorem ssubset_of_eq_of_ssubset (hab : a = b) (hbc : b ⊂ c) : a ⊂ c := by rwa [hab]

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

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

Разделы

Аффилиация

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