append_mem_append — Mathlib

English

If ma ∈ a and mb ∈ b, then ma ++ mb ∈ a ++ b, i.e. concatenating elements preserves membership in the concatenated parts.

Русский

Если ma ∈ a и mb ∈ b, то ma ++ mb ∈ a ++ b, т.е. объединение элементов сохраняет принадлежность.

LaTeX

$$$$ \forall a,b \in \mathrm{Part}(\alpha),\ \forall ma,mb \in \alpha,\ (ma \in a) \land (mb \in b) \Rightarrow (ma \!\!\!+\!\!\! mb) \in (a \!\!\!+\!\!\! b). $$$$

Lean4

theorem append_mem_append [Append α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ++ mb ∈ a ++ b := by
  simp [append_def]; aesop

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