pi_eq_empty_iff — Mathlib

English

The pi over s equals ∅ iff there exists an index i such that either α i is empty or i ∈ s and t i = ∅.

Русский

Пи по s равно пустому тогда и только тогда, когда существует i, для которого либо α i пусто, либо i ∈ s и t i = ∅.

LaTeX

$$$ s.pi t = \emptyset \iff \exists i, IsEmpty (\alpha i) \lor (i \in s \land t i = \emptyset) $$$

Lean4

theorem pi_eq_empty_iff : s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅ :=
  by
  rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
  push_neg
  refine exists_congr fun i => ?_
  cases isEmpty_or_nonempty (α i) <;> simp [*, forall_and, eq_empty_iff_forall_notMem]

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