continuousMul_inf — Mathlib

English

If two topologies t1, t2 on M both make multiplication continuous, then their infimum t1 ⊓ t2 also makes multiplication continuous.

Русский

Если две топологии t1, t2 на M делают умножение непрерывным, то их пересечение t1 ⊓ t2 тоже делает умножение непрерывным.

LaTeX

$$$\\forall h_1,h_2\\; (\\text{ContinuousMul } M) \\Rightarrow \\text{ContinuousMul } M \\text{ under } (t_1 \\inf t_2)$$$

Lean4

@[to_additive]
theorem continuousMul_inf {t₁ t₂ : TopologicalSpace M} (h₁ : @ContinuousMul M t₁ _) (h₂ : @ContinuousMul M t₂ _) :
    @ContinuousMul M (t₁ ⊓ t₂) _ := by
  rw [inf_eq_iInf]
  refine continuousMul_iInf fun b => ?_
  cases b <;> assumption

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