English
Two subtrees are disjoint iff they are not equal, provided their roots satisfy a certain nonempty condition.
Русский
Два поддерева непересекаются тогда и только тогда, когда они не равны (при условии, что корни удовлетворяют некоему условию непустоты).
LaTeX
$$Disjoint v1 v2 \\Leftrightarrow t1 \\neq t2$$
Lean4
theorem mem_subtrees_disjoint_iff {t₁ t₂ : SubRootedTree t} (ht₁ : t₁ ∈ t.subtrees) (ht₂ : t₂ ∈ t.subtrees) (v₁ v₂ : t)
(h₁ : v₁ ∈ t₁) (h₂ : v₂ ∈ t₂) : Disjoint v₁ v₂ ↔ t₁ ≠ t₂
where
mp
h := by
intro nh
have : t₁.root ≤ (v₁ : t) ⊓ (v₂ : t) := by
simp only [le_inf_iff]
exact ⟨h₁, nh ▸ h₂⟩
rw [h.eq_bot] at this
simp only [le_bot_iff] at this
exact t₁.root_ne_bot_of_mem_subtrees ht₁ this
mpr
h := by
rw [SubRootedTree.mem_iff] at h₁ h₂
contrapose! h
rw [disjoint_iff, ← ne_eq, ← bot_lt_iff_ne_bot] at h
rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh
· simp_all [RootedTree.subtrees, IsAtom.lt_iff]
rw [le_inf_iff] at oh
ext
simpa only [ht₂.le_iff_eq ht₁.1, ht₁.le_iff_eq ht₂.1, eq_comm, or_self] using le_total_of_directed oh.2 h₂
