topology_eq_inf — Mathlib

English

The topology on the units Mˣ is the infimum (greatest lower bound) of the two induced topologies, via the projection to M and via the inverse projection.

Русский

Топология мн-ва единиц Mˣ равна инфимума от двух индукций: по отображению на M и по отображению обратного образа.

LaTeX

$$instTopologicalSpaceUnits = Induced(val) ⊓ Induced(λ u : Mˣ, ↑u^{-1})$$

Lean4

@[to_additive]
theorem topology_eq_inf :
    instTopologicalSpaceUnits = .induced (val : Mˣ → M) ‹_› ⊓ .induced (fun u ↦ ↑u⁻¹ : Mˣ → M) ‹_› := by
  simp only [isInducing_embedProduct.1, instTopologicalSpaceProd, induced_inf, instTopologicalSpaceMulOpposite,
    induced_compose];
  rfl

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