eq_of_mem — Mathlib

English

Let a,b be elements of Part α. If a is defined (a.Dom) and the underlying value a.get a.Dom belongs to b, then a = b.

Русский

Пусть a, b — элементы Part α. Если a определено (a.Dom) и базовое значение a.get a.Dom принадлежит b, то a = b.

LaTeX

$$$ \forall a,b : \mathrm{Part}(\alpha),\ a.\\Dom \to a.\\get( a.\\Dom ) \in b \to a=b $$$

Lean4

theorem eq_of_mem {a b : Part α} (ha : a.Dom) (hb : a.get ha ∈ b) : a = b :=
  by
  have hb' : b.Dom := Part.dom_iff_mem.mpr ⟨a.get ha, hb⟩
  rwa [← eq_get_iff_mem hb', eq_iff_of_dom ha hb'] at hb

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