continuousInv_inf — Mathlib

English

If t1 and t2 are topologies on G and both have continuous inversion, then their meet t1 ⊓ t2 also has continuous inversion.

Русский

Если топологии t1 и t2 на G обе обеспечивают непрерывность обращения, то и их meet t1 ⊓ t2 обладает непрерывностью обращения.

LaTeX

$$$\forall t_1,t_2,\text{ContinuousInv}(G)\text{ in } t_1\land\text{ContinuousInv}(G)\text{ in } t_2\Rightarrow \text{ContinuousInv}(G)\text{ in } t_1\⊓ t_2$$$

Lean4

@[to_additive]
theorem continuousInv_inf {t₁ t₂ : TopologicalSpace G} (h₁ : @ContinuousInv G t₁ _) (h₂ : @ContinuousInv G t₂ _) :
    @ContinuousInv G (t₁ ⊓ t₂) _ := by
  rw [inf_eq_iInf]
  refine continuousInv_iInf fun b => ?_
  cases b <;> assumption

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