inter_get_eq — Mathlib

English

The get of the intersection equals the intersection of the gets: (a ∩ b).get hab = a.get(left_dom_of_inter_dom hab) ∩ b.get(right_dom_of_inter_dom hab).

Русский

Получение пересечения равно пересечению полученных значений: (a ∩ b).get hab = a.get(...) ∩ b.get(...).

LaTeX

$$$$ (a \cap b).get(hab) = a.get(left\_dom\_of\_inter\_dom(hab)) \cap b.get(right\_dom\_of\_inter\_dom(hab)). $$$$

Lean4

@[simp]
theorem inter_get_eq [Inter α] (a b : Part α) (hab : Dom (a ∩ b)) :
    (a ∩ b).get hab = a.get (left_dom_of_inter_dom hab) ∩ b.get (right_dom_of_inter_dom hab) := by simp [inter_def];
  aesop

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