inf — Mathlib

English

If two locally convex topologies t1 and t2 on E are combined by infimum, the result is locally convex.

Русский

Если две локально выпуклые топологии на E соединяются через инфимуум, результат локально выпуклый.

LaTeX

$$$\text{LocallyConvexSpace } 𝕜 E \;\Rightarrow\; (t_1 \wedge t_2) \text{ локально выпукло}$$$

Lean4

protected theorem inf {t₁ t₂ : TopologicalSpace E} (h₁ : @LocallyConvexSpace 𝕜 E _ _ _ _ t₁)
    (h₂ : @LocallyConvexSpace 𝕜 E _ _ _ _ t₂) : @LocallyConvexSpace 𝕜 E _ _ _ _ (t₁ ⊓ t₂) :=
  by
  rw [inf_eq_iInf]
  refine .iInf fun b => ?_
  cases b <;> assumption

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