continuousSMul_inf — Mathlib

English

If t1 and t2 both support a ContinuousSMul, then their infimum t1 ⊓ t2 also supports a ContinuousSMul.

Русский

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

LaTeX

$$ContinuousSMul M X on t1 ⊓ t2$$

Lean4

@[to_additive]
theorem continuousSMul_inf {t₁ t₂ : TopologicalSpace X} [@ContinuousSMul M X _ _ t₁] [@ContinuousSMul M X _ _ t₂] :
    @ContinuousSMul M X _ _ (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  refine continuousSMul_iInf fun b => ?_
  cases b <;> assumption

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