sdiff_get_eq — Mathlib

English

The get of the difference equals the difference of the gets: (a \ b).get hab = a.get(left_dom_of_sdiff_dom hab) \ b.get(right_dom_of_sdiff_dom hab).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sdiff_get_eq [SDiff α] (a b : Part α) (hab : Dom (a \ b)) :
    (a \ b).get hab = a.get (left_dom_of_sdiff_dom hab) \ b.get (right_dom_of_sdiff_dom hab) := by simp [sdiff_def];
  aesop

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