get_eq_iff_eq_some

Mathlib.Data.Part

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

English

For any a ∈ Part α, a.get ha = b iff a = some b.

Русский

Для любого a с ha ∈ Part α: a.get ha = b эквивалентно a = some(b).

LaTeX

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

Lean4

theorem get_eq_iff_eq_some {a : Part α} {ha : a.Dom} {b : α} : a.get ha = b ↔ a = some b :=
  ⟨fun h => by simp [h.symm], fun h => by simp [h]⟩

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

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

Разделы

Аффилиация

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