eq_iff_of_dom

Mathlib.Data.Part

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

English

For any a,b and domains ha,hb, a.get ha = b.get hb iff a = b.

Русский

Для любых a,b и доменов ha,hb: a.get ha = b.get hb эквивалентно a = b.

LaTeX

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

Lean4

theorem eq_iff_of_dom {a b : Part α} (ha : a.Dom) (hb : b.Dom) : a.get ha = b.get hb ↔ a = b :=
  ⟨eq_of_get_eq_get ha hb, get_eq_get_of_eq a ha⟩

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

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

Разделы

Аффилиация

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