ssubset_of_ssubset_of_eq

Mathlib.Order.RelClasses

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

English

If a ⊂ b and b = c, then a ⊂ c.

Русский

Если a ⊂ b и b = c, то a ⊂ c.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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