nonempty_pprod — Mathlib

English

Nonempty of the dependent product PProd α β is equivalent to Nonempty α and Nonempty β (the β fiber nonempty at some a).

Русский

Непусто Dependent Product PProd α β тогда и только тогда, когда непусты α и β (распределено по некоторому a).

LaTeX

$$$\operatorname{Nonempty}(\mathrm{PProd}\,\alpha\,\beta) \iff \operatorname{Nonempty} \alpha \land \operatorname{Nonempty} \beta$$$

Lean4

@[simp]
theorem nonempty_pprod {α β} : Nonempty (PProd α β) ↔ Nonempty α ∧ Nonempty β :=
  Iff.intro (fun ⟨⟨a, b⟩⟩ ↦ ⟨⟨a⟩, ⟨b⟩⟩) fun ⟨⟨a⟩, ⟨b⟩⟩ ↦ ⟨⟨a, b⟩⟩

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