trans_isLittleOTVS — Mathlib

English

IsLittleOTVS transitivity with BigOTVS in the chain

Русский

Транситивность IsLittleOTVS через цепь IsBigOTVS

LaTeX

$$trans_isLittleOTVS: $f =o_{𝕜;l} g \\to g =O_{𝕜;l} k \\Rightarrow f =o_{𝕜;l} k$$$

Lean4

theorem trans_isLittleOTVS {k : α → G} (hfg : f =O[𝕜; l] g) (hgk : g =o[𝕜; l] k) : f =o[𝕜; l] k :=
  by
  refine ⟨fun U hU₀ ↦ ?_⟩
  obtain ⟨V, hV₀, hV⟩ := hfg.1 U hU₀
  obtain ⟨W, hW₀, hW⟩ := hgk.1 V hV₀
  refine ⟨W, hW₀, fun ε hε ↦ ?_⟩
  filter_upwards [hV, hW ε hε] with x hx₁ hx₂ using hx₁.trans hx₂

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