piFinset_disjoint_of_disjoint — Mathlib

English

If for every a the sets t1(a) and t2(a) are disjoint, then piFinset t1 and piFinset t2 are disjoint.

Русский

Если для каждого a множества t1(a) и t2(a) не пересекаются, то и piFinset t1 и piFinset t2 не пересекаются.

LaTeX

$$$\\forall a,\\ \\operatorname{Disjoint}(t_1(a), t_2(a)) \\implies \\operatorname{Disjoint}(\\operatorname{piFinset} t_1, \\operatorname{piFinset} t_2).$$$

Lean4

theorem piFinset_disjoint_of_disjoint (t₁ t₂ : ∀ a, Finset (δ a)) {a : α} (h : Disjoint (t₁ a) (t₂ a)) :
    Disjoint (piFinset t₁) (piFinset t₂) :=
  disjoint_iff_ne.2 fun f₁ hf₁ f₂ hf₂ eq₁₂ =>
    disjoint_iff_ne.1 h (f₁ a) (mem_piFinset.1 hf₁ a) (f₂ a) (mem_piFinset.1 hf₂ a) (congr_fun eq₁₂ a)

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