takeUntil_takeUntil — Mathlib

English

Taking until w on p and then until x on the result equals taking until x on p with a suitable subset of the support: (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx).

Русский

Операции takeUntil дважды подряд эквивалентны взятию до x из исходного p с корректировкой поддержки: (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx).

LaTeX

$$$$ (p.takeUntil w hw).takeUntil x hx = p.takeUntil x \bigl(p.support_takeUntil_subset hw hx\bigr) $$$$

Lean4

theorem takeUntil_takeUntil {w x : V} (p : G.Walk u v) (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) :
    (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx) := by
  simp_rw [← takeUntil_append_of_mem_left _ (p.dropUntil w hw) hx, take_spec]

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