mem_union — Mathlib

English

Let s1, s2 be Finmap β. For every a : α, a ∈ s1 ∪ s2 iff a ∈ s1 or a ∈ s2.

Русский

Пусть s1, s2 — конечные отображения. Для каждого a : α верно: a ∈ s1 ∪ s2 тогда, когда a ∈ s1 или a ∈ s2.

LaTeX

$$$ a \in s_1 \cup s_2 \iff a \in s_1 \lor a \in s_2 $$$

Lean4

@[simp]
theorem mem_union {a} {s₁ s₂ : Finmap β} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ :=
  induction_on₂ s₁ s₂ fun _ _ => AList.mem_union

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