isTheta_sup — Mathlib

English

The Θ-relation along a supremum of filters is equivalent to having Θ along each component filter: f' =Θ[l ⊔ l'] g' if and only if f' =Θ[l] g' and f' =Θ[l'] g'.

Русский

Относитель Θ вдоль объединённого верхнего предела фильтров эквивалентен существованию Θ по каждому из фильтров: f' =Θ_{l ⊔ l'} g' ⇔ (f' =Θ_l g' ∧ f' =Θ_{l'} g').

LaTeX

$$$ f' =\Theta[l \sqcup l'] g' \Longleftrightarrow (f' =\Theta[l] g' \land f' =\Theta[l'] g'). $$$

Lean4

@[simp]
theorem isTheta_sup : f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g' :=
  ⟨fun h ↦ ⟨h.mono le_sup_left, h.mono le_sup_right⟩, fun h ↦ h.1.sup h.2⟩

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