isClosed_setOf_map_inv — Mathlib

English

The set of all functions f: G1 → G2 satisfying f(x^{-1}) = f(x)^{-1} for all x is closed (in the product topology).

Русский

Множество функций f: G1 → G2, удовлетворяющих f(x^{-1}) = f(x)^{-1} для всех x, является замкнутым в пространстве функций с произведной топологией.

LaTeX

$$$IsClosed \\left(\\{ f : G_1 \\to G_2 \\mid \\forall x, f(x^{-1}) = f(x)^{-1} \\} \\right).$$$

Lean4

@[to_additive]
theorem isClosed_setOf_map_inv [Inv G₁] [Inv G₂] [ContinuousInv G₂] : IsClosed {f : G₁ → G₂ | ∀ x, f x⁻¹ = (f x)⁻¹} :=
  by
  simp only [setOf_forall]
  exact isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv

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