univPi — Mathlib

English

The set Set.univ.pi s is equivalent to the dependent function type ∀ a, s(a).

Русский

Множество Set.univ.pi s эквивалентно зависимому произведению функций: ∀ a, s(a).

LaTeX

$$Set.univ.pi s \simeq \prod_{a \in \alpha} s(a)$$

Lean4

/-- The set `Set.pi Set.univ s` is equivalent to `Π a, s a`. -/
@[simps]
protected def univPi {α : Type*} {β : α → Type*} (s : ∀ a, Set (β a)) : pi univ s ≃ ∀ a, s a
    where
  toFun f a := ⟨(f : ∀ a, β a) a, f.2 a (mem_univ a)⟩
  invFun f := ⟨fun a => f a, fun a _ => (f a).2⟩

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