sigma_univ_range_eq — Mathlib

English

Let f_i be a family of maps f i: α i → β i. Then the sigma over univ of range f i equals the range of the map x ↦ ⟨x.fst, f x.fst x.snd⟩.

Русский

Пусть f_i — семейство отображений f_i: α_i → β_i. Тогда сигма над всём множеством диапазонов f_i эквивалентна диапазону отображения x ↦ ⟨x.fst, f x.fst x.snd⟩.

LaTeX

$$$\text{univ}.\sigma (\lambda i. \text{range}(f_i)) = \text{range }\lambda x: \Sigma i, \alpha i. \langle x.fst, f x.fst x.snd\rangle$$$

Lean4

theorem sigma_univ_range_eq {f : ∀ i, α i → β i} :
    (univ : Set ι).sigma (fun i ↦ range (f i)) = range fun x : Σ i, α i ↦ ⟨x.1, f _ x.2⟩ :=
  ext <| by simp [range, Sigma.forall]

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