biUnion_nonempty — Mathlib

English

The biUnion is nonempty exactly when some component is nonempty: (s.biUnion t).Nonempty ⇔ ∃ x ∈ s, (t x).Nonempty.

Русский

BiUnion непусто тогда, когда хотя бы одна компонента непустая: (s.biUnion t).Nonempty ⇔ ∃ x ∈ s, (t x).Nonempty.

LaTeX

$$$\\mathrm{Nonempty}(s.biUnion t) \\iff \\exists x \\in s,\\; \\mathrm{Nonempty}(t(x))$$$

Lean4

@[simp]
theorem biUnion_nonempty : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty :=
  by
  simp only [Finset.Nonempty, mem_biUnion]
  rw [exists_swap]
  simp [exists_and_left]

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