mem_keys_kunion — Mathlib

English

For the union of keys of l1 and l2, a is in the keys if and only if a is in the keys of l1 or in the keys of l2.

Русский

Для объединения ключей l1 и l2: a ∈ (l1.kunion l2).keys тогда и только тогда, когда a ∈ l1.keys или a ∈ l2.keys.

LaTeX

$$∀ {a} {l1 l2 : List (Σ β)}, a ∈ (l1.kunion l2).keys ↔ a ∈ l1.keys ∨ a ∈ l2.keys$$

Lean4

@[simp]
theorem mem_keys_kunion {a} {l₁ l₂ : List (Sigma β)} : a ∈ (kunion l₁ l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys := by
  induction l₁ generalizing l₂ with
  | nil => simp
  | cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

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