pi_nonempty_iff — Mathlib

English

The pi over s of t is nonempty iff for every i there exists an element of t i consistent with i ∈ s.

Русский

Произведение по s от t непусто тогда, когда для каждого i существует элемент t i, совместимый с i ∈ s.

LaTeX

$$$ (s.pi t).Nonempty \iff \forall i, \exists x, i \in s \rightarrow x \in t i $$$

Lean4

theorem pi_nonempty_iff : (s.pi t).Nonempty ↔ ∀ i, ∃ x, i ∈ s → x ∈ t i := by simp [Classical.skolem, Set.Nonempty]

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