mem_sigma — Mathlib

English

For any l1, l2, a, b, membership in the dependent sum l1.sigma l2 is characterized by membership of a in l1 and b in l2 a.

Русский

Для зависимого произведения принадлежность пары в l1.sigma l2 эквивалентна принадлежности первого компонента к l1 и второго к l2 a.

LaTeX

$$$\Sigma$-membership: $(a,b) \in l_1.sigma l_2 \iff a \in l_1 \land b \in l_2 a$$$

Lean4

@[simp]
theorem mem_sigma {l₁ : List α} {l₂ : ∀ a, List (σ a)} {a : α} {b : σ a} :
    Sigma.mk a b ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a := by
  simp [List.sigma, mem_flatMap, mem_map, exists_and_left, and_left_comm, exists_eq_left, exists_eq_right]

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