disjoint_univ_pi — Mathlib

English

Disjoint (pi univ t₁) (pi univ t₂) iff there exists i with Disjoint (t₁ i) (t₂ i).

Русский

Пусть произведение по универсууму взаимно непересекается тогда и только тогда, когда существует i такое, что t₁ i и t₂ i взаимно не пересекаются.

LaTeX

$$$ \text{Disjoint} (\pi \!\mathrm{univ} t₁) (\pi \!\mathrm{univ} t₂) \iff \exists i, \text{Disjoint} (t₁ i) (t₂ i) $$$

Lean4

@[simp]
theorem disjoint_univ_pi : Disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i) := by
  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]

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