pi_disjoint_of_disjoint — Mathlib

English

If for a ∈ s the sets t1(a) and t2(a) are disjoint, then s.pi t1 and s.pi t2 are disjoint.

Русский

Если для некоторого a ∈ s t1(a) и t2(a) дизъюнкты, то s.pi t1 и s.pi t2 дизъюнкты.

LaTeX

$$$ \\text{Disjoint}(s.\\pi t_1, s.\\pi t_2) \\; \\text{whenever } \\forall a \\in s, \\operatorname{Disjoint}(t_1(a), t_2(a)). $$$

Lean4

theorem pi_disjoint_of_disjoint {δ : α → Type*} {s : Finset α} (t₁ t₂ : ∀ a, Finset (δ a)) {a : α} (ha : a ∈ s)
    (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (s.pi t₁) (s.pi t₂) :=
  disjoint_iff_ne.2 fun f₁ hf₁ f₂ hf₂ eq₁₂ =>
    disjoint_iff_ne.1 h (f₁ a ha) (mem_pi.mp hf₁ a ha) (f₂ a ha) (mem_pi.mp hf₂ a ha) <| congr_fun (congr_fun eq₁₂ a) ha

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