instIsOpenUnitsOfContinuousInv₀OfT1Space

English

If a group with zero has aTopology making inversion continuous and is T1, then the units form an open subset.

Русский

Если группа с нулём имеет топологию, делающую непрерывной инверсию, и пространство T1, то единицы образуют открытое подмножество.

LaTeX

$$$\\mathrm{IsOpenUnits}\\, M$ подусловие: $M$ — группа с непрерывной инверсией и T1$$

Lean4

instance (priority := 900) {M : Type*} [GroupWithZero M] [TopologicalSpace M] [ContinuousInv₀ M] [T1Space M] :
    IsOpenUnits M where
  isOpenEmbedding_unitsVal := by
    refine ⟨Units.isEmbedding_val₀, ?_⟩
    convert (isClosed_singleton (X := M) (x := 0)).isOpen_compl
    ext
    simp only [Set.mem_range, Set.mem_compl_iff, Set.mem_singleton_iff]
    exact isUnit_iff_ne_zero

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