nonempty_pi — Mathlib

English

Nonempty of the function space ∀ i, α(i) is equivalent to each α(i) being nonempty.

Русский

Непусто пространство функций ∀ i, α(i) эквивалентно тому, что каждое α(i) непусто.

LaTeX

$$$\operatorname{Nonempty}(\forall i, \alpha(i)) \iff \forall i, \operatorname{Nonempty}(\alpha(i))$$$

Lean4

theorem nonempty_pi {ι} {α : ι → Sort*} : Nonempty (∀ i, α i) ↔ ∀ i, Nonempty (α i) :=
  ⟨fun ⟨f⟩ a ↦ ⟨f a⟩, @Pi.instNonempty _ _⟩

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