trans_isBigOTVS — Mathlib

English

Instance asserting that transitivity of IsLittleOTVS through IsBigOTVS holds

Русский

Экземпляр, где транситивность IsLittleOTVS через IsBigOTVS справедлива

LaTeX

$$instTransIsLittleOTVSIsBigOTVS: Trans (IsLittleOTVS 𝕜 l) (IsBigOTVS 𝕜 l) (IsLittleOTVS 𝕜 l)$$

Lean4

theorem trans_isBigOTVS {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 ε hε, hW] with x hx₁ hx₂ using hx₁.trans <| by gcongr

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