disjoint_pi — Mathlib

English

Disjoint(s.pi t1, s.pi t2) holds exactly when there exists i ∈ s with Disjoint(t1 i, t2 i).

Русский

Не пересекаются множества s.pi t1 и s.pi t2 тогда, когда существует i ∈ s, такое что t1(i) и t2(i) не пересекаются.

LaTeX

$$$ \operatorname{Disjoint}(s.\pi t_1, s.\pi t_2) \iff \exists i \in s, \operatorname{Disjoint}(t_1 i, t_2 i) $$$

Lean4

@[simp]
theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by
  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']

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