get_eq_iff_mem

Mathlib.Data.Part

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

English

For any o with Dom h, o.get h = a iff a ∈ o.

Русский

Для любого o с доменом h, o.get h = a эквивалентно a ∈ o.

LaTeX

$$$$\forall o:\mathrm{Part}\,\alpha, a:\alpha, (\mathrm{Dom}(o))\; \Rightarrow\; o.get \;{\mathrm Dom}(o) = a \iff a \in o.$$$$

Lean4

theorem get_eq_iff_mem {o : Part α} {a : α} (h : o.Dom) : o.get h = a ↔ a ∈ o :=
  ⟨fun H => ⟨h, H⟩, fun ⟨_, H⟩ => H⟩

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

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

Разделы

Аффилиация

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