get_eq_get_of_eq

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.get_eq_get_of_eq

English

If a = b then a.get ha = b.get (h ▸ ha).

Русский

Если a = b, то a.get ha = b.get (h ▸ ha).

LaTeX

$$$$\forall a:\mathrm{Part}\,\alpha, \; ha:\mathrm{Dom}(a), \forall b:\mathrm{Part}\,\alpha, \; h:\, a=b, \, a.get ha = b.get (h\,\, ha). $$$$

Lean4

theorem get_eq_get_of_eq (a : Part α) (ha : a.Dom) {b : Part α} (h : a = b) : a.get ha = b.get (h ▸ ha) := by congr

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

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

Разделы

Аффилиация

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