Mathlib.Topology.Algebra.Support

mulTSupport definition

(f : X → α) : Set X

Full source

/-- The topological support of a function is the closure of its support, i.e. the closure of the
set of all elements where the function is not equal to 1. -/
@[to_additive "The topological support of a function is the closure of its support. i.e. the
closure of the set of all elements where the function is nonzero."]
def mulTSupport (f : X → α) : Set X := closure (mulSupport f)

Topological multiplicative support of a function

Informal description

For a function $ f : X \to \alpha $, the topological support $\text{mulTSupport}(f)$ is defined as the closure of the multiplicative support of $ f $, where the multiplicative support is the set of all points $ x \in X $ such that $ f(x) \neq 1 $.

subset_mulTSupport theorem

(f : X → α) : mulSupport f ⊆ mulTSupport f

Full source

@[to_additive]
theorem subset_mulTSupport (f : X → α) : mulSupportmulSupport f ⊆ mulTSupport f :=
  subset_closure

Multiplicative support is contained in its topological support

Informal description

For any function $f : X \to \alpha$, the multiplicative support of $f$ (the set of points where $f(x) \neq 1$) is a subset of its topological multiplicative support (the closure of the multiplicative support).

isClosed_mulTSupport theorem

(f : X → α) : IsClosed (mulTSupport f)

Full source

@[to_additive]
theorem isClosed_mulTSupport (f : X → α) : IsClosed (mulTSupport f) :=
  isClosed_closure

Topological Multiplicative Support is Closed

Informal description

For any function $ f : X \to \alpha $, the topological multiplicative support $\text{mulTSupport}(f)$ is a closed subset of $X$.

mulTSupport_eq_empty_iff theorem

{f : X → α} : mulTSupport f = ∅ ↔ f = 1

Full source

@[to_additive]
theorem mulTSupport_eq_empty_iff {f : X → α} : mulTSupportmulTSupport f = ∅ ↔ f = 1 := by
  rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]

Characterization of Empty Topological Multiplicative Support: $\text{mulTSupport}(f) = \emptyset \leftrightarrow f = 1$

Informal description

For a function $f : X \to \alpha$, the topological multiplicative support $\text{mulTSupport}(f)$ is empty if and only if $f$ is identically equal to the multiplicative identity $1$ on $X$.

image_eq_one_of_nmem_mulTSupport theorem

{f : X → α} {x : X} (hx : x ∉ mulTSupport f) : f x = 1

Full source

@[to_additive]
theorem image_eq_one_of_nmem_mulTSupport {f : X → α} {x : X} (hx : x ∉ mulTSupport f) : f x = 1 :=
  mulSupport_subset_iff'.mp (subset_mulTSupport f) x hx

Function Value is One Outside Topological Multiplicative Support

Informal description

For a function $f : X \to \alpha$ and a point $x \in X$, if $x$ does not belong to the topological multiplicative support of $f$ (i.e., $x \notin \text{mulTSupport}(f)$), then $f(x) = 1$.

range_subset_insert_image_mulTSupport theorem

(f : X → α) : range f ⊆ insert 1 (f '' mulTSupport f)

Full source

@[to_additive]
theorem range_subset_insert_image_mulTSupport (f : X → α) :
    rangerange f ⊆ insert 1 (f '' mulTSupport f) :=
  (range_subset_insert_image_mulSupport f).trans <|
    insert_subset_insert <| image_subset _ subset_closure

Range of Function is Subset of Unit Union Image of Topological Support

Informal description

For any function $f : X \to \alpha$, the range of $f$ is contained in the union of $\{1\}$ and the image of the topological multiplicative support of $f$ under $f$. In other words, $\text{range}(f) \subseteq \{1\} \cup f(\text{mulTSupport}(f))$.

range_eq_image_mulTSupport_or theorem

(f : X → α) : range f = f '' mulTSupport f ∨ range f = insert 1 (f '' mulTSupport f)

Full source

@[to_additive]
theorem range_eq_image_mulTSupport_or (f : X → α) :
    rangerange f = f '' mulTSupport f ∨ range f = insert 1 (f '' mulTSupport f) :=
  (wcovBy_insert _ _).eq_or_eq (image_subset_range _ _) (range_subset_insert_image_mulTSupport f)

Range Characterization via Topological Multiplicative Support

Informal description

For any function $f : X \to \alpha$, the range of $f$ is either equal to the image of its topological multiplicative support under $f$, or it is equal to the union of $\{1\}$ and the image of the topological multiplicative support under $f$. In other words, $\text{range}(f) = f(\text{mulTSupport}(f))$ or $\text{range}(f) = \{1\} \cup f(\text{mulTSupport}(f))$.

tsupport_mul_subset_left theorem

{α : Type*} [MulZeroClass α] {f g : X → α} : (tsupport fun x => f x * g x) ⊆ tsupport f

Full source

theorem tsupport_mul_subset_left {α : Type*} [MulZeroClass α] {f g : X → α} :
    (tsupport fun x => f x * g x) ⊆ tsupport f :=
  closure_mono (support_mul_subset_left _ _)

Topological support of product is contained in support of left factor

Informal description

For any functions $f, g : X \to \alpha$ where $\alpha$ is a `MulZeroClass`, the topological support of the pointwise product $f \cdot g$ is contained in the topological support of $f$. In other words, $\text{tsupport}(f \cdot g) \subseteq \text{tsupport}(f)$.

tsupport_mul_subset_right theorem

{α : Type*} [MulZeroClass α] {f g : X → α} : (tsupport fun x => f x * g x) ⊆ tsupport g

Full source

theorem tsupport_mul_subset_right {α : Type*} [MulZeroClass α] {f g : X → α} :
    (tsupport fun x => f x * g x) ⊆ tsupport g :=
  closure_mono (support_mul_subset_right _ _)

Inclusion of Topological Support for Right Factor in Product Function

Informal description

Let $X$ be a topological space and $\alpha$ be a type with a multiplication operation and a zero element (i.e., a `MulZeroClass` structure). For any two functions $f, g : X \to \alpha$, the topological support of the product function $x \mapsto f(x) \cdot g(x)$ is contained in the topological support of $g$.

tsupport_smul_subset_left theorem

 {M α} [TopologicalSpace X] [Zero M] [Zero α] [SMulWithZero M α] (f : X → M) (g : X → α) :
  (tsupport fun x => f x • g x) ⊆ tsupport f

Full source

theorem tsupport_smul_subset_left {M α} [TopologicalSpace X] [Zero M] [Zero α] [SMulWithZero M α]
    (f : X → M) (g : X → α) : (tsupport fun x => f x • g x) ⊆ tsupport f :=
  closure_mono <| support_smul_subset_left f g

Topological support of scalar multiplication is contained in support of left factor

Informal description

Let $X$ be a topological space, and let $M$ and $\alpha$ be types with zero elements. Suppose $\alpha$ has a scalar multiplication operation by $M$ that preserves zero (i.e., $0 \cdot x = 0$ and $m \cdot 0 = 0$ for all $m \in M$ and $x \in \alpha$). For any functions $f \colon X \to M$ and $g \colon X \to \alpha$, the topological support of the function $x \mapsto f(x) \cdot g(x)$ is contained in the topological support of $f$.

tsupport_smul_subset_right theorem

 {M α} [TopologicalSpace X] [Zero α] [SMulZeroClass M α] (f : X → M) (g : X → α) :
  (tsupport fun x => f x • g x) ⊆ tsupport g

Full source

theorem tsupport_smul_subset_right {M α} [TopologicalSpace X] [Zero α] [SMulZeroClass M α]
    (f : X → M) (g : X → α) : (tsupport fun x => f x • g x) ⊆ tsupport g :=
  closure_mono <| support_smul_subset_right f g

Topological support of scalar multiplication is contained in support of right operand

Informal description

Let $X$ be a topological space, $\alpha$ be a type with a zero element, and $M$ be a type equipped with a scalar multiplication operation `SMulZeroClass M α`. For any functions $f : X \to M$ and $g : X \to \alpha$, the topological support of the function $x \mapsto f(x) \cdot g(x)$ is contained in the topological support of $g$.

mulTSupport_mul theorem

 [TopologicalSpace X] [MulOneClass α] {f g : X → α} : (mulTSupport fun x ↦ f x * g x) ⊆ mulTSupport f ∪ mulTSupport g

Full source

@[to_additive]
theorem mulTSupport_mul [TopologicalSpace X] [MulOneClass α] {f g : X → α} :
    (mulTSupport fun x ↦ f x * g x) ⊆ mulTSupport f ∪ mulTSupport g :=
  closure_minimal
    ((mulSupport_mul f g).trans (union_subset_union (subset_mulTSupport _) (subset_mulTSupport _)))
    (isClosed_closure.union isClosed_closure)

Topological support of product is contained in union of supports

Informal description

Let $X$ be a topological space and $\alpha$ be a multiplicative monoid. For any functions $f, g : X \to \alpha$, the topological multiplicative support of the product function $x \mapsto f(x) \cdot g(x)$ is contained in the union of the topological multiplicative supports of $f$ and $g$.

not_mem_mulTSupport_iff_eventuallyEq theorem

: x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1

Full source

@[to_additive]
theorem not_mem_mulTSupport_iff_eventuallyEq : x ∉ mulTSupport fx ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1 := by
  simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]

Characterization of Points Outside the Topological Multiplicative Support via Eventual Equality to One

Informal description

A point $x$ is not in the topological multiplicative support of a function $f$ if and only if $f$ is eventually equal to $1$ in a neighborhood of $x$.

continuous_of_mulTSupport theorem

[TopologicalSpace β] {f : α → β} (hf : ∀ x ∈ mulTSupport f, ContinuousAt f x) : Continuous f

Full source

@[to_additive]
theorem continuous_of_mulTSupport [TopologicalSpace β] {f : α → β}
    (hf : ∀ x ∈ mulTSupport f, ContinuousAt f x) : Continuous f :=
  continuous_iff_continuousAt.2 fun x => (em _).elim (hf x) fun hx =>
    (@continuousAt_const _ _ _ _ _ 1).congr (not_mem_mulTSupport_iff_eventuallyEq.mp hx).symm

Continuity via Continuity on Topological Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces. If $f$ is continuous at every point in its topological multiplicative support $\text{mulTSupport}(f)$, then $f$ is continuous everywhere.

ContinuousOn.continuous_of_mulTSupport_subset theorem

 [TopologicalSpace β] {f : α → β} {s : Set α} (hs : ContinuousOn f s) (h's : IsOpen s) (h''s : mulTSupport f ⊆ s) :
  Continuous f

Full source

@[to_additive]
lemma ContinuousOn.continuous_of_mulTSupport_subset [TopologicalSpace β] {f : α → β}
    {s : Set α} (hs : ContinuousOn f s) (h's : IsOpen s) (h''s : mulTSupportmulTSupport f ⊆ s) :
    Continuous f :=
  continuous_of_mulTSupport fun _ hx ↦ h's.continuousOn_iff.mp hs <| h''s hx

Global Continuity via Continuity on Open Set Containing Topological Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $s \subseteq \alpha$ be an open set. If $f$ is continuous on $s$ and the topological multiplicative support of $f$ is contained in $s$, then $f$ is continuous on the whole space $\alpha$.

HasCompactMulSupport definition

(f : α → β) : Prop

Full source

/-- A function `f` *has compact multiplicative support* or is *compactly supported* if the closure
of the multiplicative support of `f` is compact. In a T₂ space this is equivalent to `f` being equal
to `1` outside a compact set. -/
@[to_additive "A function `f` *has compact support* or is *compactly supported* if the closure of
the support of `f` is compact. In a T₂ space this is equivalent to `f` being equal to `0` outside a
compact set."]
def HasCompactMulSupport (f : α → β) : Prop :=
  IsCompact (mulTSupport f)

Function with compact multiplicative support

Informal description

A function $ f : \alpha \to \beta $ is said to have *compact multiplicative support* if the closure of its multiplicative support (the set of points where $ f(x) \neq 1 $) is a compact set. In a T₂ space, this is equivalent to $ f $ being equal to $ 1 $ outside some compact set.

hasCompactMulSupport_def theorem

: HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))

Full source

@[to_additive]
theorem hasCompactMulSupport_def : HasCompactMulSupportHasCompactMulSupport f ↔ IsCompact (closure (mulSupport f)) := by
  rfl

Characterization of Compact Multiplicative Support via Closure

Informal description

A function $f : \alpha \to \beta$ has compact multiplicative support if and only if the closure of its multiplicative support $\{x \mid f(x) \neq 1\}$ is a compact set.

exists_compact_iff_hasCompactMulSupport theorem

[R1Space α] : (∃ K : Set α, IsCompact K ∧ ∀ x, x ∉ K → f x = 1) ↔ HasCompactMulSupport f

Full source

@[to_additive]
theorem exists_compact_iff_hasCompactMulSupport [R1Space α] :
    (∃ K : Set α, IsCompact K ∧ ∀ x, x ∉ K → f x = 1) ↔ HasCompactMulSupport f := by
  simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]

Characterization of Functions with Compact Multiplicative Support in R₁ Spaces

Informal description

Let $\alpha$ be an R₁ space and $f : \alpha \to \beta$ a function. Then there exists a compact set $K \subseteq \alpha$ such that $f(x) = 1$ for all $x \notin K$ if and only if $f$ has compact multiplicative support.

HasCompactMulSupport.intro theorem

[R1Space α] {K : Set α} (hK : IsCompact K) (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f

Full source

@[to_additive]
theorem intro [R1Space α] {K : Set α} (hK : IsCompact K)
    (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f :=
  exists_compact_iff_hasCompactMulSupport.mp ⟨K, hK, hfK⟩

Compact Support Implies Compact Multiplicative Support in R₁ Spaces

Informal description

Let $\alpha$ be an R₁ space and $f : \alpha \to \beta$ a function. If there exists a compact set $K \subseteq \alpha$ such that $f(x) = 1$ for all $x \notin K$, then $f$ has compact multiplicative support.

HasCompactMulSupport.intro' theorem

{K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f

Full source

@[to_additive]
theorem intro' {K : Set α} (hK : IsCompact K) (h'K : IsClosed K)
    (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f := by
  have : mulTSupportmulTSupport f ⊆ K := by
    rw [← h'K.closure_eq]
    apply closure_mono (mulSupport_subset_iff'.2 hfK)
  exact IsCompact.of_isClosed_subset hK ( isClosed_mulTSupport f) this

Compact-Closed Set Condition for Compact Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a function, and let $K \subseteq \alpha$ be a subset that is both compact and closed. If $f(x) = 1$ for all $x \notin K$, then $f$ has compact multiplicative support.

HasCompactMulSupport.of_mulSupport_subset_isCompact theorem

[R1Space α] {K : Set α} (hK : IsCompact K) (h : mulSupport f ⊆ K) : HasCompactMulSupport f

Full source

@[to_additive]
theorem of_mulSupport_subset_isCompact [R1Space α] {K : Set α}
    (hK : IsCompact K) (h : mulSupportmulSupport f ⊆ K) : HasCompactMulSupport f :=
  hK.closure_of_subset h

Compact Containment Implies Compact Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a function on an R₁ space $\alpha$. If the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) is contained in a compact subset $K$ of $\alpha$, then $f$ has compact multiplicative support.

HasCompactMulSupport.isCompact theorem

(hf : HasCompactMulSupport f) : IsCompact (mulTSupport f)

Full source

@[to_additive]
theorem isCompact (hf : HasCompactMulSupport f) : IsCompact (mulTSupport f) :=
  hf

Compactness of Topological Multiplicative Support for Functions with Compact Multiplicative Support

Informal description

If a function $f : X \to \alpha$ has compact multiplicative support, then its topological multiplicative support $\text{mulTSupport}(f)$ (the closure of the set $\{x \in X \mid f(x) \neq 1\}$) is compact.

hasCompactMulSupport_iff_eventuallyEq theorem

: HasCompactMulSupport f ↔ f =ᶠ[coclosedCompact α] 1

Full source

@[to_additive]
theorem _root_.hasCompactMulSupport_iff_eventuallyEq :
    HasCompactMulSupportHasCompactMulSupport f ↔ f =ᶠ[coclosedCompact α] 1 :=
  mem_coclosedCompact_iff.symm

Characterization of Compact Multiplicative Support via Eventual Equality to One

Informal description

A function $f : \alpha \to \beta$ has compact multiplicative support if and only if $f$ is eventually equal to $1$ on the coclosed compact filter of $\alpha$.

isCompact_range_of_mulSupport_subset_isCompact theorem

 [TopologicalSpace β] (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : mulSupport f ⊆ k) : IsCompact (range f)

Full source

@[to_additive]
theorem _root_.isCompact_range_of_mulSupport_subset_isCompact [TopologicalSpace β]
    (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : mulSupportmulSupport f ⊆ k) :
    IsCompact (range f) := by
  rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2 <;> rw [h2]
  exacts [hk.image hf, (hk.image hf).insert 1]

Compactness of Range for Functions with Compact Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a continuous function between topological spaces, and let $k \subseteq \alpha$ be a compact set. If the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) is contained in $k$, then the range of $f$ is compact.

HasCompactMulSupport.isCompact_range theorem

[TopologicalSpace β] (h : HasCompactMulSupport f) (hf : Continuous f) : IsCompact (range f)

Full source

@[to_additive]
theorem isCompact_range [TopologicalSpace β] (h : HasCompactMulSupport f)
    (hf : Continuous f) : IsCompact (range f) :=
  isCompact_range_of_mulSupport_subset_isCompact hf h (subset_mulTSupport f)

Compactness of Range for Functions with Compact Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a continuous function between topological spaces. If $f$ has compact multiplicative support, then the range of $f$ is compact.

HasCompactMulSupport.mono' theorem

{f' : α → γ} (hf : HasCompactMulSupport f) (hff' : mulSupport f' ⊆ mulTSupport f) : HasCompactMulSupport f'

Full source

@[to_additive]
theorem mono' {f' : α → γ} (hf : HasCompactMulSupport f)
    (hff' : mulSupportmulSupport f' ⊆ mulTSupport f) : HasCompactMulSupport f' :=
  IsCompact.of_isClosed_subset hf isClosed_closure <| closure_minimal hff' isClosed_closure

Inheritance of Compact Multiplicative Support under Containment of Supports

Informal description

Let $f : \alpha \to \beta$ be a function with compact multiplicative support, and let $f' : \alpha \to \gamma$ be another function such that the multiplicative support of $f'$ is contained in the topological multiplicative support of $f$. Then $f'$ also has compact multiplicative support.

HasCompactMulSupport.mono theorem

{f' : α → γ} (hf : HasCompactMulSupport f) (hff' : mulSupport f' ⊆ mulSupport f) : HasCompactMulSupport f'

Full source

@[to_additive]
theorem mono {f' : α → γ} (hf : HasCompactMulSupport f)
    (hff' : mulSupportmulSupport f' ⊆ mulSupport f) : HasCompactMulSupport f' :=
  hf.mono' <| hff'.trans subset_closure

Inheritance of Compact Multiplicative Support under Containment of Multiplicative Supports

Informal description

Let $f : \alpha \to \beta$ be a function with compact multiplicative support, and let $f' : \alpha \to \gamma$ be another function such that the multiplicative support of $f'$ is contained in the multiplicative support of $f$. Then $f'$ also has compact multiplicative support.

HasCompactMulSupport.comp_left theorem

(hf : HasCompactMulSupport f) (hg : g 1 = 1) : HasCompactMulSupport (g ∘ f)

Full source

@[to_additive]
theorem comp_left (hf : HasCompactMulSupport f) (hg : g 1 = 1) :
    HasCompactMulSupport (g ∘ f) :=
  hf.mono <| mulSupport_comp_subset hg f

Composition preserves compact multiplicative support when $g(1) = 1$

Informal description

Let $f : \alpha \to \beta$ be a function with compact multiplicative support, and let $g : \beta \to \gamma$ be a function satisfying $g(1) = 1$. Then the composition $g \circ f$ also has compact multiplicative support.

hasCompactMulSupport_comp_left theorem

(hg : ∀ {x}, g x = 1 ↔ x = 1) : HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f

Full source

@[to_additive]
theorem _root_.hasCompactMulSupport_comp_left (hg : ∀ {x}, g x = 1 ↔ x = 1) :
    HasCompactMulSupportHasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f := by
  simp_rw [hasCompactMulSupport_def, mulSupport_comp_eq g (@hg) f]

Compact Multiplicative Support under Composition with Bijective Condition at One

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions such that $g(x) = 1$ if and only if $x = 1$. Then the composition $g \circ f$ has compact multiplicative support if and only if $f$ has compact multiplicative support.

HasCompactMulSupport.comp_isClosedEmbedding theorem

(hf : HasCompactMulSupport f) {g : α' → α} (hg : IsClosedEmbedding g) : HasCompactMulSupport (f ∘ g)

Full source

@[to_additive]
theorem comp_isClosedEmbedding (hf : HasCompactMulSupport f) {g : α' → α}
    (hg : IsClosedEmbedding g) : HasCompactMulSupport (f ∘ g) := by
  rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
  refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_
  rw [hg.isEmbedding.closure_eq_preimage_closure_image]
  exact preimage_mono (closure_mono <| image_preimage_subset _ _)

Composition Preserves Compact Multiplicative Support under Closed Embedding

Informal description

Let $f : \alpha \to \beta$ be a function with compact multiplicative support, and let $g : \alpha' \to \alpha$ be a closed embedding. Then the composition $f \circ g$ also has compact multiplicative support.

HasCompactMulSupport.comp₂_left theorem

 (hf : HasCompactMulSupport f) (hf₂ : HasCompactMulSupport f₂) (hm : m 1 1 = 1) :
  HasCompactMulSupport fun x => m (f x) (f₂ x)

Full source

@[to_additive]
theorem comp₂_left (hf : HasCompactMulSupport f)
    (hf₂ : HasCompactMulSupport f₂) (hm : m 1 1 = 1) :
    HasCompactMulSupport fun x => m (f x) (f₂ x) := by
  rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢
  filter_upwards [hf, hf₂] with x hx hx₂
  simp_rw [hx, hx₂, Pi.one_apply, hm]

Compact Multiplicative Support under Binary Operation

Informal description

Let $f, f_2 : \alpha \to \beta$ be functions with compact multiplicative support, and let $m : \beta \to \beta \to \beta$ be a binary operation such that $m(1,1) = 1$. Then the function $x \mapsto m(f(x), f_2(x))$ also has compact multiplicative support.

HasCompactMulSupport.isCompact_preimage theorem

 [TopologicalSpace β] (h'f : HasCompactMulSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k) (h'k : 1 ∉ k) :
  IsCompact (f ⁻¹' k)

Full source

@[to_additive]
lemma isCompact_preimage [TopologicalSpace β]
    (h'f : HasCompactMulSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k)
    (h'k : 1 ∉ k) : IsCompact (f ⁻¹' k) := by
  apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)
  apply subset_mulTSupport
  aesop

Compactness of Preimage under Function with Compact Multiplicative Support

Informal description

Let $f : \alpha \to \beta$ be a continuous function with compact multiplicative support, and let $k \subseteq \beta$ be a closed set not containing the multiplicative identity $1$. Then the preimage $f^{-1}(k)$ is compact.

HasCompactMulSupport.mulTSupport_extend_one_subset theorem

: mulTSupport (g.extend f 1) ⊆ g '' mulTSupport f

Full source

@[to_additive]
theorem mulTSupport_extend_one_subset :
    mulTSupportmulTSupport (g.extend f 1) ⊆ g '' mulTSupport f :=
  (hf.image cont).isClosed.closure_subset_iff.mpr <|
    mulSupport_extend_one_subset.trans (image_subset g subset_closure)

Inclusion of Supports for Extended Function: $\text{mulTSupport}(g.extend\ f\ 1) \subseteq g(\text{mulTSupport}(f))$

Informal description

For functions $f : X \to \alpha$ and $g : Y \to X$, the topological multiplicative support of the extended function $g.extend\ f\ 1$ is contained in the image under $g$ of the topological multiplicative support of $f$. In other words, $$\text{mulTSupport}(g.extend\ f\ 1) \subseteq g(\text{mulTSupport}(f))$$ where $\text{mulTSupport}(f)$ denotes the closure of the set $\{x \in X \mid f(x) \neq 1\}$.

HasCompactMulSupport.extend_one theorem

: HasCompactMulSupport (g.extend f 1)

Full source

@[to_additive]
theorem extend_one : HasCompactMulSupport (g.extend f 1) :=
  HasCompactMulSupport.of_mulSupport_subset_isCompact (hf.image cont)
    (subset_closure.trans <| hf.mulTSupport_extend_one_subset cont)

Compact Multiplicative Support of Extended Function by One

Informal description

For functions $f : X \to \alpha$ and $g : Y \to X$, the extended function $g.extend\ f\ 1$ (which extends $f$ by 1 outside the image of $g$) has compact multiplicative support.

HasCompactMulSupport.mulTSupport_extend_one theorem

(inj : g.Injective) : mulTSupport (g.extend f 1) = g '' mulTSupport f

Full source

@[to_additive]
theorem mulTSupport_extend_one (inj : g.Injective) :
    mulTSupport (g.extend f 1) = g '' mulTSupport f :=
  (hf.mulTSupport_extend_one_subset cont).antisymm <|
    (image_closure_subset_closure_image cont).trans
      (closure_mono (mulSupport_extend_one inj).superset)

Equality of Supports for Injective Extension: $\text{mulTSupport}(g.extend\ f\ 1) = g(\text{mulTSupport}(f))$

Informal description

Let $f : X \to \alpha$ and $g : Y \to X$ be functions, where $g$ is injective. Then the topological multiplicative support of the extended function $g.extend\ f\ 1$ (which extends $f$ by 1 outside the image of $g$) is equal to the image under $g$ of the topological multiplicative support of $f$. That is, $$\text{mulTSupport}(g.extend\ f\ 1) = g(\text{mulTSupport}(f))$$ where $\text{mulTSupport}(f)$ denotes the closure of $\{x \in X \mid f(x) \neq 1\}$.

HasCompactMulSupport.continuous_extend_one theorem

 [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : U → β} (cont : Continuous f) (supp : HasCompactMulSupport f) :
  Continuous (Subtype.val.extend f 1)

Full source

@[to_additive]
theorem continuous_extend_one [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : U → β}
    (cont : Continuous f) (supp : HasCompactMulSupport f) :
    Continuous (Subtype.val.extend f 1) :=
  continuous_of_mulTSupport fun x h ↦ by
    rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _
      (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,
      ← (hU.isOpenEmbedding_subtypeVal).continuousAt_iff, extend_comp Subtype.val_injective]
    exact cont.continuousAt

Continuity of Extension by One for Functions with Compact Multiplicative Support

Informal description

Let $U$ be an open subset of a topological space $\alpha'$, and let $f \colon U \to \beta$ be a continuous function with compact multiplicative support. Then the extension of $f$ by $1$ to the entire space $\alpha'$ (defined by setting $f(x) = 1$ for $x \notin U$) is continuous.

HasCompactMulSupport.is_one_at_infty theorem

{f : α → γ} [TopologicalSpace γ] (h : HasCompactMulSupport f) : Tendsto f (cocompact α) (𝓝 1)

Full source

/-- If `f` has compact multiplicative support, then `f` tends to 1 at infinity. -/
@[to_additive "If `f` has compact support, then `f` tends to zero at infinity."]
theorem is_one_at_infty {f : α → γ} [TopologicalSpace γ]
    (h : HasCompactMulSupport f) : Tendsto f (cocompact α) (𝓝 1) := by
  intro N hN
  rw [mem_map, mem_cocompact']
  refine ⟨mulTSupport f, h.isCompact, ?_⟩
  rw [compl_subset_comm]
  intro v hv
  rw [mem_preimage, image_eq_one_of_nmem_mulTSupport hv]
  exact mem_of_mem_nhds hN

Functions with Compact Multiplicative Support Tend to One at Infinity

Informal description

For a function $f \colon \alpha \to \gamma$ with compact multiplicative support, $f$ tends to $1$ at infinity, i.e., $\lim_{x \to \infty} f(x) = 1$.

HasCompactMulSupport.of_compactSpace theorem

(f : α → γ) : HasCompactMulSupport f

Full source

/-- In a compact space `α`, any function has compact support. -/
@[to_additive]
theorem HasCompactMulSupport.of_compactSpace (f : α → γ) :
    HasCompactMulSupport f :=
  IsCompact.of_isClosed_subset isCompact_univ (isClosed_mulTSupport f)
    (Set.subset_univ (mulTSupport f))

Functions on Compact Spaces Have Compact Multiplicative Support

Informal description

If $\alpha$ is a compact space, then any function $f \colon \alpha \to \gamma$ has compact multiplicative support.

HasCompactMulSupport.mul theorem

(hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') : HasCompactMulSupport (f * f')

Full source

@[to_additive]
theorem HasCompactMulSupport.mul (hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') :
    HasCompactMulSupport (f * f') := hf.comp₂_left hf' (mul_one 1)

Product of Functions with Compact Multiplicative Support

Informal description

If two functions $f, f' \colon \alpha \to \beta$ have compact multiplicative support, then their pointwise product $f \cdot f'$ also has compact multiplicative support.

HasCompactMulSupport.one theorem

{α β : Type*} [TopologicalSpace α] [One β] : HasCompactMulSupport (1 : α → β)

Full source

@[to_additive, simp]
protected lemma HasCompactMulSupport.one {α β : Type*} [TopologicalSpace α] [One β] :
    HasCompactMulSupport (1 : α → β) := by
  simp [HasCompactMulSupport, mulTSupport]

Constant One Function Has Compact Multiplicative Support

Informal description

For any topological space $\alpha$ and any type $\beta$ with a multiplicative identity $1$, the constant function $1 : \alpha \to \beta$ has compact multiplicative support.

HasCompactMulSupport.inv' theorem

 {α β : Type*} [TopologicalSpace α] [DivisionMonoid β] {f : α → β} (hf : HasCompactMulSupport f) :
  HasCompactMulSupport (f⁻¹)

Full source

@[to_additive]
protected lemma HasCompactMulSupport.inv' {α β : Type*} [TopologicalSpace α] [DivisionMonoid β]
    {f : α → β} (hf : HasCompactMulSupport f) :
    HasCompactMulSupport (f⁻¹) := by
  simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv'] using hf

Compact multiplicative support is preserved under inversion

Informal description

Let $\alpha$ be a topological space and $\beta$ be a division monoid. If a function $f : \alpha \to \beta$ has compact multiplicative support, then its multiplicative inverse $f^{-1}$ also has compact multiplicative support.

HasCompactSupport.smul_left theorem

(hf : HasCompactSupport f') : HasCompactSupport (f • f')

Full source

theorem HasCompactSupport.smul_left (hf : HasCompactSupport f') : HasCompactSupport (f • f') := by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]

Compact support is preserved under left scalar multiplication

Informal description

Let $\alpha$ be a topological space and $\beta$ be a module over a ring. If a function $f' : \alpha \to \beta$ has compact support, then for any function $f : \alpha \to \beta$, the function $f \cdot f'$ (scalar multiplication of $f$ and $f'$) also has compact support.

HasCompactSupport.smul_right theorem

(hf : HasCompactSupport f) : HasCompactSupport (f • f')

Full source

theorem HasCompactSupport.smul_right (hf : HasCompactSupport f) : HasCompactSupport (f • f') := by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Compact support is preserved under right scalar multiplication

Informal description

Let $\alpha$ be a topological space and $\beta$ be a module over a ring. If a function $f : \alpha \to \beta$ has compact support, then for any function $f' : \alpha \to \beta$, the function $f \smul f'$ (scalar multiplication of $f$ and $f'$) also has compact support.

HasCompactSupport.mul_right theorem

(hf : HasCompactSupport f) : HasCompactSupport (f * f')

Full source

theorem HasCompactSupport.mul_right (hf : HasCompactSupport f) : HasCompactSupport (f * f') := by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]

Compact support is preserved under right multiplication

Informal description

Let $f, f' : \alpha \to \beta$ be functions from a topological space $\alpha$ to a ring $\beta$. If $f$ has compact support, then the product function $f \cdot f'$ also has compact support.

HasCompactSupport.mul_left theorem

(hf : HasCompactSupport f') : HasCompactSupport (f * f')

Full source

theorem HasCompactSupport.mul_left (hf : HasCompactSupport f') : HasCompactSupport (f * f') := by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

Compact support is preserved under left multiplication

Informal description

Let $f, f' : \alpha \to \beta$ be functions from a topological space $\alpha$ to a ring $\beta$. If $f'$ has compact support, then the product function $f \cdot f'$ also has compact support.

HasCompactSupport.abs theorem

{f : α → β} (hf : HasCompactSupport f) : HasCompactSupport |f|

Full source

protected theorem HasCompactSupport.abs {f : α → β} (hf : HasCompactSupport f) :
    HasCompactSupport |f| :=
  hf.comp_left (g := abs) abs_zero

Compact support is preserved under absolute value

Informal description

Let $f : \alpha \to \beta$ be a function from a topological space $\alpha$ to a normed space $\beta$. If $f$ has compact support, then the absolute value function $|f|$ also has compact support.

LocallyFinite.exists_finset_nhd_mulSupport_subset theorem

 {U : ι → Set X} [One R] {f : ι → X → R} (hlf : LocallyFinite fun i => mulSupport (f i))
  (hso : ∀ i, mulTSupport (f i) ⊆ U i) (ho : ∀ i, IsOpen (U i)) (x : X) :
  ∃ (is : Finset ι), ∃ n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ i ∈ is, U i) ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ is

Full source

/-- If a family of functions `f` has locally-finite multiplicative support, subordinate to a family
of open sets, then for any point we can find a neighbourhood on which only finitely-many members of
`f` are not equal to 1. -/
@[to_additive "If a family of functions `f` has locally-finite support, subordinate to a family of
open sets, then for any point we can find a neighbourhood on which only finitely-many members of `f`
are non-zero."]
theorem LocallyFinite.exists_finset_nhd_mulSupport_subset {U : ι → Set X} [One R] {f : ι → X → R}
    (hlf : LocallyFinite fun i => mulSupport (f i)) (hso : ∀ i, mulTSupportmulTSupport (f i) ⊆ U i)
    (ho : ∀ i, IsOpen (U i)) (x : X) :
    ∃ (is : Finset ι), ∃ n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ i ∈ is, U i) ∧
      ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ is := by
  obtain ⟨n, hn, hnf⟩ := hlf x
  classical
    let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.not_mem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
      intro i hi
      simp only [Finite.coe_toFinset, mem_setOf_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩

Local Finiteness of Multiplicative Support Yields Finite Neighborhood Support

Informal description

Let $X$ be a topological space, $\iota$ an index set, and $R$ a type with a multiplicative identity $1$. Consider a family of functions $f_i : X \to R$ indexed by $i \in \iota$ such that the family of multiplicative supports $\{x \in X \mid f_i(x) \neq 1\}$ is locally finite. Suppose for each $i$, the topological multiplicative support $\text{mulTSupport}(f_i)$ (the closure of $\text{mulSupport}(f_i)$) is contained in an open set $U_i \subseteq X$. Then for any point $x \in X$, there exists a finite subset $I \subseteq \iota$ and a neighborhood $N$ of $x$ such that: 1. $N \subseteq \bigcap_{i \in I} U_i$ 2. For all $z \in N$, the multiplicative support $\{i \in \iota \mid f_i(z) \neq 1\}$ is contained in $I$.

locallyFinite_mulSupport_iff theorem

 [One M] {f : ι → X → M} : (LocallyFinite fun i ↦ mulSupport <| f i) ↔ LocallyFinite fun i ↦ mulTSupport <| f i

Full source

@[to_additive]
theorem locallyFinite_mulSupport_iff [One M] {f : ι → X → M} :
    (LocallyFinite fun i ↦ mulSupport <| f i) ↔ LocallyFinite fun i ↦ mulTSupport <| f i :=
  ⟨LocallyFinite.closure, fun H ↦ H.subset fun _ ↦ subset_closure⟩

Equivalence of Local Finiteness for Multiplicative Support and Topological Multiplicative Support

Informal description

For a family of functions $ f_i : X \to M $ indexed by $ i \in \iota $, where $ M $ has a multiplicative identity, the family of multiplicative supports $ \text{mulSupport}(f_i) $ is locally finite if and only if the family of topological multiplicative supports $ \text{mulTSupport}(f_i) $ is locally finite.

LocallyFinite.smul_left theorem

 [Zero R] [Zero M] [SMulWithZero R M] {s : ι → X → R} (h : LocallyFinite fun i ↦ support <| s i) (f : ι → X → M) :
  LocallyFinite fun i ↦ support <| s i • f i

Full source

theorem LocallyFinite.smul_left [Zero R] [Zero M] [SMulWithZero R M]
    {s : ι → X → R} (h : LocallyFinite fun i ↦ support <| s i) (f : ι → X → M) :
    LocallyFinite fun i ↦ support <| s i • f i :=
  h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, zero_smul]

Local Finiteness of Supports under Scalar Multiplication

Informal description

Let $R$ and $M$ be types with zero elements, equipped with a scalar multiplication operation `[SMulWithZero R M]`. Given a family of functions $s_i : X \to R$ indexed by $i \in \iota$ and a family of functions $f_i : X \to M$, if the supports of the functions $s_i$ are locally finite, then the supports of the scalar products $s_i \cdot f_i$ are also locally finite.

LocallyFinite.smul_right theorem

 [Zero M] [SMulZeroClass R M] {f : ι → X → M} (h : LocallyFinite fun i ↦ support <| f i) (s : ι → X → R) :
  LocallyFinite fun i ↦ support <| s i • f i

Full source

theorem LocallyFinite.smul_right [Zero M] [SMulZeroClass R M]
    {f : ι → X → M} (h : LocallyFinite fun i ↦ support <| f i) (s : ι → X → R) :
    LocallyFinite fun i ↦ support <| s i • f i :=
  h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, smul_zero]

Local Finiteness of Supports under Right Scalar Multiplication

Informal description

Let $M$ be a type with a zero element and a scalar multiplication operation `[SMulZeroClass R M]`. Given a family of functions $f_i : X \to M$ indexed by $i \in \iota$ such that the supports of the $f_i$ are locally finite, and a family of scalar functions $s_i : X \to R$, then the supports of the scalar products $s_i \cdot f_i$ are also locally finite.

HasCompactMulSupport.comp_homeomorph theorem

{M} [One M] {f : Y → M} (hf : HasCompactMulSupport f) (φ : X ≃ₜ Y) : HasCompactMulSupport (f ∘ φ)

Full source

@[to_additive]
theorem HasCompactMulSupport.comp_homeomorph {M} [One M] {f : Y → M}
    (hf : HasCompactMulSupport f) (φ : X ≃ₜ Y) : HasCompactMulSupport (f ∘ φ) :=
  hf.comp_isClosedEmbedding φ.isClosedEmbedding

Composition with Homeomorphism Preserves Compact Multiplicative Support

Informal description

Let $M$ be a type with a distinguished element $1$, and let $f : Y \to M$ be a function with compact multiplicative support. If $\phi : X \to Y$ is a homeomorphism, then the composition $f \circ \phi : X \to M$ also has compact multiplicative support.

Mathlib.Topology.Algebra.Support

Main definitions

TODO