`BookProof.ChapterMackeyInducedSystem.inducedSystem_fibre` (L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)) (s : X → G) (hs : ∀ x, s x • x₀ = x) (f : FieldSpace X K) : (inducedSyste

Proved

BookProof.ChapterMackeyInducedSystem.inducedSystem_fibre

by leonardopedro · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMackeyInducedSystem.

BookProof.ChapterMackeyInducedSystem.inducedSystem_fibre (L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)) (s : X → G) (hs : ∀ x, s x • x₀ = x) (f : FieldSpace X K) : (inducedSystem L s hs).p x₀ f = f ↔ ∀ x, x ≠ x₀ → f x = 0

Formalization note: Lean 4 identifier BookProof.ChapterMackeyInducedSystem.inducedSystem_fibre.

Preamble

-- Generated from ChapterMackeyInducedSystem.lean — theorem BookProof.ChapterMackeyInducedSystem.inducedSystem_fibre
import Definitions.Def_ChapterMackeyImprimitivity
import Mathlib
import Definitions.Def_ChapterMackeyInducedSystem
open BookProof.ChapterMackeyInducedSystem


open scoped InnerProductSpace
open Finset


open BookProof.ChapterMackeyImprimitivity

variable {G : Type*} [Group G] {X : Type*} [Fintype X] [DecidableEq X] [MulAction G X]
variable {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
variable {x₀ : X}

variable {L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)} {s : X → G}
variable (L s)
variable {L s}
variable (X K) in

Formal statement

theorem BookProof.ChapterMackeyInducedSystem.inducedSystem_fibre (L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)) (s : X → G)
    (hs : ∀ x, s x • x₀ = x) (f : FieldSpace X K) :
    (inducedSystem L s hs).p x₀ f = f ↔ ∀ x, x ≠ x₀ → f x = 0 := by sorry

View graph