append_get_eq — Mathlib

English

If a ++ b is defined, then the value of (a ++ b) at its domain is the concatenation of the values of a and b at their respective domains.

Русский

Если a ++ b определено, то значение (a ++ b) в их доменных точках равно конкатенации значений a и b в их доменах.

LaTeX

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

Lean4

@[simp]
theorem append_get_eq [Append α] (a b : Part α) (hab : Dom (a ++ b)) :
    (a ++ b).get hab = a.get (left_dom_of_append_dom hab) ++ b.get (right_dom_of_append_dom hab) := by
  simp [append_def]; aesop

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