nonempty_sigma — Mathlib

English

Nonempty of the dependent sum equals existence of index with nonempty fiber.

Русский

Непусто зависимого суммирования эквивалентно существованию индекса с непустым волокном.

LaTeX

$$$\operatorname{Nonempty}(\Sigma a : \alpha, \gamma a) \iff \exists a : \alpha, \operatorname{Nonempty}(\gamma a)$$$

Lean4

@[simp]
theorem nonempty_sigma : Nonempty (Σ a : α, γ a) ↔ ∃ a : α, Nonempty (γ a) :=
  Iff.intro (fun ⟨⟨a, c⟩⟩ ↦ ⟨a, ⟨c⟩⟩) fun ⟨a, ⟨c⟩⟩ ↦ ⟨⟨a, c⟩⟩

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