English
For a finite set s and nonempty filtered support, there exists a distinguished x ∈ s whose support contains all t ∈ s that appear in the takeUntil-x prefix only if t = x.
Русский
Для конечного множества s и не пустого фильтрованного множества поддержки, существует особая вершина x ∈ s, такая что каждая t ∈ s, встречающаяся в префиксе takeUntil x, равно x.
LaTeX
$$$ (s : Finset V) (h : {x \in s | x \in p.support}.Nonempty) : \exists x \in s, \exists hx : x \in p.support, \forall t \in s, t \in (p.takeUntil x hx).support \rightarrow t = x $$$
Lean4
theorem exists_mem_support_forall_mem_support_imp_eq (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) :
∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x :=
by
obtain ⟨x, hxs, hx, h⟩ := p.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty s h
use x, hxs, hx
suffices {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ { x } by simpa [Finset.subset_iff] using this
rwa [Finset.filter_erase, ← Finset.subset_empty, ← Finset.subset_insert_iff, LawfulSingleton.insert_empty_eq] at h
