union_get_eq — Mathlib

English

The get of the union equals the union of the gets: (a ∪ b).get hab = a.get(left_dom_of_union_dom hab) ∪ b.get(right_dom_of_union_dom hab).

Русский

Получение по объединению равно объединению полученных значений двух частей.

LaTeX

$$$$ (a \cup b).get(hab) = a.get(left\_dom\_of\_union\_dom hab) \cup b.get(right\_dom\_of\_union\_dom hab). $$$$

Lean4

@[simp]
theorem union_get_eq [Union α] (a b : Part α) (hab : Dom (a ∪ b)) :
    (a ∪ b).get hab = a.get (left_dom_of_union_dom hab) ∪ b.get (right_dom_of_union_dom hab) := by simp [union_def];
  aesop

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