pi_nonempty — Mathlib

English

The pi set s.pi t is nonempty if and only if every a ∈ s has t(a) nonempty.

Русский

Множество s.pi t непустое тогда и только тогда, когда для каждого a ∈ s множество t(a) непусто.

LaTeX

$$$ (s.\\pi t).\\mathrm{Nonempty} \\;\\iff \\; \\forall a \\in s, (t a).Nonempty. $$$

Lean4

@[simp]
theorem pi_nonempty : (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty := by simp [Finset.Nonempty, Classical.skolem]

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