isLittleOTVS_sup — Mathlib

English

The IsLittleOTVS relation with respect to the supremum of two filters is equivalent to the conjunction of the relations with respect to each filter separately.

Русский

Отношение IsLittleOTVS относительно объединения фильтров равносильно сочетанию отношений по каждому фильтру отдельно.

LaTeX

$$$\\text{IsLittleOTVS}(\\\\mathfrak{k}, l_1 \\sqcup l_2, f, g) \\iff \\text{IsLittleOTVS}(\\\\mathfrak{k}, l_1, f, g) \\land \\text{IsLittleOTVS}(\\\\mathfrak{k}, l_2, f, g).$$$

Lean4

theorem isLittleOTVS_sup : f =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g := by
  simp only [isLittleOTVS_iff_smallSets, ← forall_and, ← eventually_and, eventually_sup]

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