subtrees_disjoint — Mathlib

English

The family of subtrees is pairwise disjoint as sets of nodes.

Русский

Множество поддеревьев парно попарно непересекается как множества узлов.

LaTeX

$$t.subtrees.PairwiseDisjoint ((↑) : _ → Set t)$$

Lean4

theorem subtrees_disjoint : t.subtrees.PairwiseDisjoint ((↑) : _ → Set t) :=
  by
  intro t₁ ht₁ t₂ ht₂ h
  rw [Function.onFun_apply, Set.disjoint_left]
  intro a ha hb
  rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h
  subst h
  simp only [SetLike.mem_coe, SubRootedTree.bot_mem_iff] at ha
  exact t₁.root_ne_bot_of_mem_subtrees ht₁ ha

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