Documentation

theorem ContinuousInv.induced {α : Type u_4} {β : Type u_5} {F : Type u_6} [FunLike F α β] [Group α] [DivisionMonoid β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousInv β] (f : F) :

ContinuousInv α

theorem ContinuousNeg.induced {α : Type u_4} {β : Type u_5} {F : Type u_6} [FunLike F α β] [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousNeg β] (f : F) :

ContinuousNeg α

theorem Specializes.inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x y : G} (h : x ⤳ y) :

x⁻¹ ⤳ y⁻¹

theorem Specializes.neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x y : G} (h : x ⤳ y) :

(-x) ⤳ (-y)

theorem Inseparable.inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x y : G} (h : Inseparable x y) :

Inseparable x⁻¹ y⁻¹

theorem Inseparable.neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x y : G} (h : Inseparable x y) :

Inseparable (-x) (-y)

theorem Specializes.zpow {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G} (h : x ⤳ y) (m : ℤ) :

(x ^ m) ⤳ (y ^ m)

theorem Specializes.zsmul {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x y : G} (h : x ⤳ y) (m : ℤ) :

(m • x) ⤳ (m • y)

theorem Inseparable.zpow {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G} (h : Inseparable x y) (m : ℤ) :

Inseparable (x ^ m) (y ^ m)

theorem Inseparable.zsmul {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x y : G} (h : Inseparable x y) (m : ℤ) :

Inseparable (m • x) (m • y)

instance instContinuousInvULift {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] :

ContinuousInv (ULift.{u_4, u_1} G)

instance instContinuousNegULift {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] :

ContinuousNeg (ULift.{u_4, u_1} G)

theorem continuousOn_inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} :

ContinuousOn Inv.inv s

theorem continuousOn_neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} :

ContinuousOn Neg.neg s

theorem continuousWithinAt_inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} {x : G} :

ContinuousWithinAt Inv.inv s x

theorem continuousWithinAt_neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} {x : G} :

ContinuousWithinAt Neg.neg s x

theorem continuousAt_inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} :

ContinuousAt Inv.inv x

theorem continuousAt_neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} :

ContinuousAt Neg.neg x

theorem tendsto_inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] (a : G) :

Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹)

theorem tendsto_neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (a : G) :

Filter.Tendsto Neg.neg (nhds a) (nhds (-a))

instance OrderDual.instContinuousInv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] :

ContinuousInv Gᵒᵈ

instance OrderDual.instContinuousNeg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] :

ContinuousNeg Gᵒᵈ

instance Prod.continuousInv {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace H] [Inv H] [ContinuousInv H] :

ContinuousInv (G × H)

instance Prod.continuousNeg {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace H] [Neg H] [ContinuousNeg H] :

ContinuousNeg (G × H)

instance Pi.continuousInv {ι : Type u_4} {C : ι → Type u_5} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Inv (C i)] [∀ (i : ι), ContinuousInv (C i)] :

ContinuousInv ((i : ι) → C i)

instance Pi.continuousNeg {ι : Type u_4} {C : ι → Type u_5} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] :

ContinuousNeg ((i : ι) → C i)

instance Pi.has_continuous_inv' {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {ι : Type u_4} :

ContinuousInv (ι → G)

A version of Pi.continuousInv for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousInv for non-dependent functions.

instance Pi.has_continuous_neg' {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {ι : Type u_4} :

ContinuousNeg (ι → G)

A version of Pi.continuousNeg for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousNeg for non-dependent functions.

@[instance 100]

instance continuousInv_of_discreteTopology {H : Type u_2} [TopologicalSpace H] [Inv H] [DiscreteTopology H] :

ContinuousInv H

@[instance 100]

instance continuousNeg_of_discreteTopology {H : Type u_2} [TopologicalSpace H] [Neg H] [DiscreteTopology H] :

ContinuousNeg H

@[instance 100]

instance continuousInv_of_indiscreteTopology {H : Type u_2} [TopologicalSpace H] [Inv H] [IndiscreteTopology H] :

ContinuousInv H

@[instance 100]

instance continuousNeg_of_indiscreteTopology {H : Type u_2} [TopologicalSpace H] [Neg H] [IndiscreteTopology H] :

ContinuousNeg H

@[instance 100]

instance continuousDiv_of_discreteTopology {H : Type u_2} [TopologicalSpace H] [Div H] [DiscreteTopology H] :

ContinuousDiv H

@[instance 100]

instance continuousSub_of_discreteTopology {H : Type u_2} [TopologicalSpace H] [Sub H] [DiscreteTopology H] :

ContinuousSub H

@[instance 100]

instance continuousDiv_of_indiscreteTopology {H : Type u_2} [TopologicalSpace H] [Div H] [IndiscreteTopology H] :

ContinuousDiv H

@[instance 100]

instance continuousSub_of_indiscreteTopology {H : Type u_2} [TopologicalSpace H] [Sub H] [IndiscreteTopology H] :

ContinuousSub H

@[instance 100]

instance topologicalGroup_of_discreteTopology {H : Type u_2} [TopologicalSpace H] [Group H] [DiscreteTopology H] :

IsTopologicalGroup H

@[instance 100]

instance topologicalAddGroup_of_discreteTopology {H : Type u_2} [TopologicalSpace H] [AddGroup H] [DiscreteTopology H] :

IsTopologicalAddGroup H

@[instance 100]

instance topologicalGroup_of_indiscreteTopology {H : Type u_2} [TopologicalSpace H] [Group H] [IndiscreteTopology H] :

IsTopologicalGroup H

@[instance 100]

instance topologicalAddGroup_of_indiscreteTopology {H : Type u_2} [TopologicalSpace H] [AddGroup H] [IndiscreteTopology H] :

IsTopologicalAddGroup H

theorem isClosed_setOfPred_map_inv (G₁ : Type u_5) (G₂ : Type u_6) [TopologicalSpace G₂] [T2Space G₂] [Inv G₁] [Inv G₂] [ContinuousInv G₂] :

IsClosed {f : G₁ → G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

theorem isClosed_setOfPred_map_neg (G₁ : Type u_5) (G₂ : Type u_6) [TopologicalSpace G₂] [T2Space G₂] [Neg G₁] [Neg G₂] [ContinuousNeg G₂] :

IsClosed {f : G₁ → G₂ | ∀ (x : G₁), f (-x) = -f x}

@[deprecated isClosed_setOfPred_map_inv (since := "2026-07-09")]

theorem isClosed_setOf_map_inv (G₁ : Type u_5) (G₂ : Type u_6) [TopologicalSpace G₂] [T2Space G₂] [Inv G₁] [Inv G₂] [ContinuousInv G₂] :

IsClosed {f : G₁ → G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

Alias of isClosed_setOfPred_map_inv.

@[deprecated isClosed_setOfPred_map_neg (since := "2026-07-09")]

theorem isClosed_setOf_map_neg (G₁ : Type u_5) (G₂ : Type u_6) [TopologicalSpace G₂] [T2Space G₂] [Neg G₁] [Neg G₂] [ContinuousNeg G₂] :

IsClosed {f : G₁ → G₂ | ∀ (x : G₁), f (-x) = -f x}

Alias of isClosed_setOfPred_map_neg.

instance instContinuousNegAdditiveOfContinuousInv {H : Type u_2} [TopologicalSpace H] [Inv H] [ContinuousInv H] :

ContinuousNeg (Additive H)

instance instContinuousInvMultiplicativeOfContinuousNeg {H : Type u_2} [TopologicalSpace H] [Neg H] [ContinuousNeg H] :

ContinuousInv (Multiplicative H)

@[simp]

theorem tendsto_inv_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {l : Filter α} {m : α → G} {a : G} :

Filter.Tendsto (fun (x : α) => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)

@[simp]

theorem tendsto_neg_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {l : Filter α} {m : α → G} {a : G} :

Filter.Tendsto (fun (x : α) => -m x) l (nhds (-a)) ↔ Filter.Tendsto m l (nhds a)

theorem IsCompact.inv {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsCompact s) :

IsCompact s⁻¹

theorem IsCompact.neg {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsCompact s) :

IsCompact (-s)

def Homeomorph.inv (G : Type u_4) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

G ≃ₜ G

Inversion in a topological group as a homeomorphism.

Equations

Homeomorph.inv G = { toEquiv := Equiv.inv G, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

def Homeomorph.neg (G : Type u_4) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] :

G ≃ₜ G

Negation in a topological group as a homeomorphism.

Equations

Homeomorph.neg G = { toEquiv := Equiv.neg G, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

@[simp]

theorem Homeomorph.symm_inv {G : Type u_4} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

(Homeomorph.inv G).symm = Homeomorph.inv G

@[simp]

theorem Homeomorph.symm_neg {G : Type u_4} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] :

(Homeomorph.neg G).symm = Homeomorph.neg G

@[simp]

theorem Homeomorph.coe_inv {G : Type u_4} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

⇑(Homeomorph.inv G) = Inv.inv

@[simp]

theorem Homeomorph.coe_neg {G : Type u_4} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] :

⇑(Homeomorph.neg G) = Neg.neg

theorem nhds_inv (G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (a : G) :

nhds a⁻¹ = (nhds a)⁻¹

theorem nhds_neg (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (a : G) :

nhds (-a) = -nhds a

theorem isOpenMap_inv (G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

IsOpenMap Inv.inv

theorem isOpenMap_neg (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] :

IsOpenMap Neg.neg

theorem isClosedMap_inv (G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

IsClosedMap Inv.inv

theorem isClosedMap_neg (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] :

IsClosedMap Neg.neg

theorem IsOpen.inv {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsOpen s) :

IsOpen s⁻¹

theorem IsOpen.neg {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsOpen s) :

IsOpen (-s)

theorem IsClosed.inv {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsClosed s) :

IsClosed s⁻¹

theorem IsClosed.neg {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsClosed s) :

IsClosed (-s)

theorem inv_closure {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (s : Set G) :

(closure s)⁻¹ = closure s⁻¹

theorem neg_closure {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (s : Set G) :

-closure s = closure (-s)

@[simp]

theorem continuous_inv_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} :

Continuous f⁻¹ ↔ Continuous f

@[simp]

theorem continuous_neg_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} :

Continuous (-f) ↔ Continuous f

@[simp]

theorem continuousAt_inv_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} :

ContinuousAt f⁻¹ x ↔ ContinuousAt f x

@[simp]

theorem continuousAt_neg_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {x : α} :

ContinuousAt (-f) x ↔ ContinuousAt f x

@[simp]

theorem continuousOn_inv_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} :

ContinuousOn f⁻¹ s ↔ ContinuousOn f s

@[simp]

theorem continuousOn_neg_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {s : Set α} :

ContinuousOn (-f) s ↔ ContinuousOn f s

theorem Continuous.of_inv {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} :

Continuous f⁻¹ → Continuous f

Alias of the forward direction of continuous_inv_iff.

theorem Continuous.of_neg {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} :

Continuous (-f) → Continuous f

Alias of the forward direction of continuous_neg_iff.

theorem ContinuousAt.of_inv {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} :

ContinuousAt f⁻¹ x → ContinuousAt f x

Alias of the forward direction of continuousAt_inv_iff.

theorem ContinuousAt.of_neg {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {x : α} :

ContinuousAt (-f) x → ContinuousAt f x

Alias of the forward direction of continuousAt_neg_iff.

theorem ContinuousOn.of_inv {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} :

ContinuousOn f⁻¹ s → ContinuousOn f s

Alias of the forward direction of continuousOn_inv_iff.

theorem ContinuousOn.of_neg {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {s : Set α} :

ContinuousOn (-f) s → ContinuousOn f s

Alias of the forward direction of continuousOn_neg_iff.

@[simp]

theorem Filter.inv_nhdsNE {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {a : G} :

(nhdsWithin a {a}ᶜ)⁻¹ = nhdsWithin a⁻¹ {a⁻¹ }ᶜ

@[simp]

theorem Filter.neg_nhdsNE {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {a : G} :

-nhdsWithin a {a}ᶜ = nhdsWithin (-a) {-a}ᶜ

theorem continuousInv_sInf {G : Type u_1} [Inv G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, ContinuousInv G) :

theorem continuousNeg_sInf {G : Type u_1} [Neg G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, ContinuousNeg G) :

theorem continuousInv_iInf {G : Type u_1} {ι' : Sort u_4} [Inv G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousInv G) :

theorem continuousNeg_iInf {G : Type u_1} {ι' : Sort u_4} [Neg G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousNeg G) :

theorem continuousInv_inf {G : Type u_1} [Inv G] {t₁ t₂ : TopologicalSpace G} (h₁ : ContinuousInv G) (h₂ : ContinuousInv G) :

theorem continuousNeg_inf {G : Type u_1} [Neg G] {t₁ t₂ : TopologicalSpace G} (h₁ : ContinuousNeg G) (h₂ : ContinuousNeg G) :

theorem Topology.IsInducing.continuousInv {G : Type u_4} {H : Type u_5} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H] {f : G → H} (hf : IsInducing f) (hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹) :

theorem Topology.IsInducing.continuousNeg {G : Type u_4} {H : Type u_5} [Neg G] [Neg H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousNeg H] {f : G → H} (hf : IsInducing f) (hf_neg : ∀ (x : G), f (-x) = -f x) :