Locally Constant Compactly Supported Functions

This file defines locally constant and compactly supported complex-valued functions on a totally disconnected locally compact Hausdorff space.

structure LocConst_td (X : Type u_1) [TopologicalSpace X] : Type u_1

Locally constant ℂ-valued functions on X.

• toFun : X → ℂ
• locallyConstant' : IsLocallyConstant self.toFun

instance LocConst_td.instFunLikeComplex (X : Type u_1) [TopologicalSpace X] : FunLike (LocConst_td X) X ℂ

Equations

• LocConst_td.instFunLikeComplex X = { coe := LocConst_td.toFun, coe_injective' := ⋯ }

@[simp]

theorem LocConst_td.toFun_eq_coe (X : Type u_1) [TopologicalSpace X] (f : LocConst_td X) : f.toFun = ⇑f

theorem LocConst_td.locallyConstant (X : Type u_1) [TopologicalSpace X] (f : LocConst_td X) : IsLocallyConstant ⇑f

theorem LocConst_td.ext (X : Type u_1) [TopologicalSpace X] {f g : LocConst_td X} (h : ∀ (x : X), f x = g x) : f = g

theorem LocConst_td.ext_iff {X : Type u_1} [TopologicalSpace X] {f g : LocConst_td X} : f = g ↔ ∀ (x : X), f x = g x

structure CptSupportLocConst_td (X : Type u_1) [TopologicalSpace X] extends LocConst_td X : Type u_1

Compactly supported locally constant ℂ-valued functions on X.

• toFun : X → ℂ
• locallyConstant' : IsLocallyConstant self.toFun
• hasCompactSupport' : HasCompactSupport self.toFun

instance CptSupportLocConst_td.instFunLikeComplex (X : Type u_1) [TopologicalSpace X] : FunLike (CptSupportLocConst_td X) X ℂ

Equations

• CptSupportLocConst_td.instFunLikeComplex X = { coe := fun (f : CptSupportLocConst_td X) => f.toFun, coe_injective' := ⋯ }

@[simp]

theorem CptSupportLocConst_td.toFun_eq_coe (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : f.toFun = ⇑f

theorem CptSupportLocConst_td.locallyConstant (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : IsLocallyConstant ⇑f

theorem CptSupportLocConst_td.hasCompactSupport (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : HasCompactSupport ⇑f

Basic facts about Function.support

theorem CptSupportLocConst_td.support_eq_preimage (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : Function.support ⇑f = ⇑f ⁻¹' {0}ᶜ

theorem CptSupportLocConst_td.support_compl_eq_preimage (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : (Function.support ⇑f)ᶜ = ⇑f ⁻¹' {0}

theorem CptSupportLocConst_td.isOpen_support (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : IsOpen (Function.support ⇑f)

theorem CptSupportLocConst_td.isOpen_support_compl (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : IsOpen (Function.support ⇑f)ᶜ

theorem CptSupportLocConst_td.isClosed_support (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : IsClosed (Function.support ⇑f)

theorem CptSupportLocConst_td.isClopen_support (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : IsClopen (Function.support ⇑f)

theorem CptSupportLocConst_td.isCompact_support (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : IsCompact (Function.support ⇑f)

theorem CptSupportLocConst_td.ext (X : Type u_1) [TopologicalSpace X] {f g : CptSupportLocConst_td X} (h : ∀ (x : X), f x = g x) : f = g

theorem CptSupportLocConst_td.ext_iff {X : Type u_1} [TopologicalSpace X] {f g : CptSupportLocConst_td X} : f = g ↔ ∀ (x : X), f x = g x

instance CptSupportLocConst_td.instZero (X : Type u_1) [TopologicalSpace X] : Zero (CptSupportLocConst_td X)

Zero function is locally constant with compact support.

Equations

• CptSupportLocConst_td.instZero X = { zero := let __LocConst_td := { toFun := 0, locallyConstant' := ⋯ }; { toLocConst_td := __LocConst_td, hasCompactSupport' := ⋯ } }

@[simp]

theorem CptSupportLocConst_td.coe_zero (X : Type u_1) [TopologicalSpace X] : ⇑0 = 0

instance CptSupportLocConst_td.instAdd (X : Type u_1) [TopologicalSpace X] : Add (CptSupportLocConst_td X)

Addition of compactly supported locally constant functions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CptSupportLocConst_td.coe_add (X : Type u_1) [TopologicalSpace X] (f g : CptSupportLocConst_td X) : ⇑(f + g) = ⇑f + ⇑g

instance CptSupportLocConst_td.instNeg (X : Type u_1) [TopologicalSpace X] : Neg (CptSupportLocConst_td X)

Negation of compactly supported locally constant functions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CptSupportLocConst_td.coe_neg (X : Type u_1) [TopologicalSpace X] (f : CptSupportLocConst_td X) : ⇑(-f) = -⇑f

instance CptSupportLocConst_td.instSMulComplex (X : Type u_1) [TopologicalSpace X] : SMul ℂ (CptSupportLocConst_td X)

Scalar multiplication of compactly supported locally constant functions by ℂ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CptSupportLocConst_td.coe_smul (X : Type u_1) [TopologicalSpace X] (c : ℂ) (f : CptSupportLocConst_td X) : ⇑(c • f) = c • ⇑f

noncomputable instance CptSupportLocConst_td.instAddCommGroup (X : Type u_1) [TopologicalSpace X] : AddCommGroup (CptSupportLocConst_td X)

CptSupportLocConst_td X is an additive commutative group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CptSupportLocConst_td.instModuleComplex (X : Type u_1) [TopologicalSpace X] : Module ℂ (CptSupportLocConst_td X)

CptSupportLocConst_td X is a ℂ-module.

Equations

• CptSupportLocConst_td.instModuleComplex X = { toSMul := CptSupportLocConst_td.instSMulComplex X, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }