set_pi — Mathlib

English

Let s ⊆ ι. If i ∈ s and t1(i) and t2(i) are disjoint, then the Pi-product sets s · π t1 and s · π t2 are disjoint.

Русский

Пусть s ⊆ ι. Если i ∈ s и t1(i) и t2(i) непересекаются, то множества s · π t1 и s · π t2 попарно непересекаются.

LaTeX

$$$ i \in s \land \operatorname{Disjoint}(t_1(i), t_2(i)) \Rightarrow \operatorname{Disjoint}(s \pi t_1, s \pi t_2) $$$

Lean4

theorem set_pi (hi : i ∈ s) (ht : Disjoint (t₁ i) (t₂ i)) : Disjoint (s.pi t₁) (s.pi t₂) :=
  disjoint_left.2 fun _ h₁ h₂ => disjoint_left.1 ht (h₁ _ hi) (h₂ _ hi)

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