subset_of_subset_of_eq

Mathlib.Order.RelClasses

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

English

Let α be a type with subset relation. If a ⊆ b and b = c, then a ⊆ c.

Русский

Пусть α — тип с отношением включения. Если a ⊆ b и b = c, то a ⊆ c.

LaTeX

$$$a \subseteq b \to b = c \to a \subseteq c$$$

Lean4

theorem subset_of_subset_of_eq (hab : a ⊆ b) (hbc : b = c) : a ⊆ c := by rwa [← hbc]

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

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

Разделы

Аффилиация

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