coe_sigma — Mathlib

English

The coercion of sigma matches the sigma constructed from coerced components.

Русский

К обоcобразованию сигма совпадает с сигмой, построенной из приведённых компонент.

LaTeX

$$$ (s.sigma t : Set (\Sigma i, \alpha i)) = (s : Set ι).sigma (\lambda i, (t i : Set (\alpha i))) $$$

Lean4

@[simp, norm_cast]
theorem coe_sigma (s : Finset ι) (t : ∀ i, Finset (α i)) :
    (s.sigma t : Set (Σ i, α i)) = (s : Set ι).sigma fun i ↦ (t i : Set (α i)) :=
  Set.ext fun _ => mem_sigma

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