LocallyConstant.ext
theorem LocallyConstant.ext :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] ⦃f g : LocallyConstant X Y⦄,
(∀ (x : X), f x = g x) → f = g
This theorem states that for any two locally constant functions `f` and `g` from a topological space `X` to any type `Y`, if these two functions agree on every point in `X` (i.e., for each `x` in `X`, `f(x) = g(x)`), then `f` and `g` are the same function. In other words, two locally constant functions are considered identical if they produce the same value for every input in the underlying topological space.
More concisely: If two locally constant functions from a topological space to a type have the same value at every point, then they are equal.
|
IsLocallyConstant.iff_eventually_eq
theorem IsLocallyConstant.iff_eventually_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y),
IsLocallyConstant f ↔ ∀ (x : X), ∀ᶠ (y : X) in nhds x, f y = f x
The theorem `IsLocallyConstant.iff_eventually_eq` asserts that for all types `X` and `Y` where `X` is a topological space and `f` is a function from `X` to `Y`, the function `f` is locally constant (the preimage of any set under `f` is an open set) if and only if for every `x` in `X`, eventually (meaning for all points `y` in the neighborhood of `x`), the value of `f` at `y` is equal to the value of `f` at `x`. In other words, a function is locally constant if the function's value remains the same in a neighborhood around each point.
More concisely: A function between topological spaces is locally constant if and only if for each point in the domain, its image value is eventually constant in every neighborhood of that point.
|
Mathlib.Topology.LocallyConstant.Basic._auxLemma.7
theorem Mathlib.Topology.LocallyConstant.Basic._auxLemma.7 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
The theorem `Mathlib.Topology.LocallyConstant.Basic._auxLemma.7` states that for all types `α` and `β`, a function `f` from `α` to `β`, a set `s` of type `β`, and an element `a` of type `α`, the element `a` belongs to the preimage of the set `s` under the function `f` if and only if the function `f` evaluated at `a` belongs to the set `s`. In mathematical terms, this can be represented as \(a \in f^{-1}(s)\) if and only if \(f(a) \in s\). This theorem establishes the relationship between the preimage of a set under a function and the function's value at a particular point.
More concisely: For all types `α` and `β`, function `f` from `α` to `β`, set `s` of type `β`, and element `a` of type `α`, `a` is in the preimage of `s` under `f` if and only if `f(a)` is in `s`. In symbols, `a ∈ f⁻¹(s)` if and only if `f(a) ∈ s`.
|
LocallyConstant.isLocallyConstant
theorem LocallyConstant.isLocallyConstant :
∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] (self : LocallyConstant X Y),
IsLocallyConstant self.toFun
The theorem `LocallyConstant.isLocallyConstant` states that for any types `X` and `Y`, along with a topological space instance on `X`, if `self` is a locally constant function from `X` to `Y`, then `self.toFun` satisfies the property of being a locally constant function. In other words, for any set `s` in the codomain `Y`, the preimage of `s` under `self.toFun` is an open set in the domain `X`.
More concisely: If `self` is a locally constant function from a topological space `X` to `Y`, then the image of every open set in `X` under `self.toFun` is an open set in `Y`.
|
IsLocallyConstant.const
theorem IsLocallyConstant.const :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (y : Y), IsLocallyConstant (Function.const X y) := by
sorry
This theorem states that for any given types `X` and `Y`, with `X` being a topological space, and any element `y` of `Y`, the function that is constantly `y` (i.e., the function that maps every element of `X` to `y`) is a locally constant function. Here, a function is said to be locally constant if, for any set in `Y`, its preimage under the function is an open set in `X`. That means, regardless of how we choose a set in `Y`, when we look at all the points in `X` that map into this set, they form an open set.
More concisely: For any topological space X and any element y in a type Y, the constant function from X to y is locally constant.
|
IsLocallyConstant.comp
theorem IsLocallyConstant.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] {f : X → Y},
IsLocallyConstant f → ∀ (g : Y → Z), IsLocallyConstant (g ∘ f)
The theorem `IsLocallyConstant.comp` states that for any three types `X`, `Y`, and `Z`, given a topological space over `X` and a function `f` from `X` to `Y` that is locally constant — meaning the preimage of any subset of `Y` under `f` is an open set in `X` — then for any function `g` from `Y` to `Z`, the composition of `g` and `f` (denoted as `g ∘ f`) is also locally constant. Essentially, this means the property of being locally constant is preserved under function composition.
More concisely: If `f : X -> Y` is locally constant and `g : Y -> Z`, then `g ∘ f` is locally constant.
|
IsLocallyConstant.iff_continuous
theorem IsLocallyConstant.iff_continuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {x : TopologicalSpace Y} [inst_1 : DiscreteTopology Y]
(f : X → Y), IsLocallyConstant f ↔ Continuous f
This theorem states that for any function `f` from a topological space `X` to another topological space `Y` (where `Y` has a discrete topology), `f` is locally constant if and only if `f` is a continuous function. In other words, a function between topological spaces is locally constant (i.e., the preimage of any set is open) if and only if it is continuous, given that the codomain has a discrete topology.
More concisely: A function from a topological space to a discrete topological space is locally constant if and only if it is continuous.
|
IsLocallyConstant.apply_eq_of_isPreconnected
theorem IsLocallyConstant.apply_eq_of_isPreconnected :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
IsLocallyConstant f → ∀ {s : Set X}, IsPreconnected s → ∀ {x y : X}, x ∈ s → y ∈ s → f x = f y
This theorem states that if a function is locally constant on a topological space, then it is constant over any preconnected subset of this space. More concretely, for any two elements in the preconnected subset, the function will take on the same value. This holds for all topological spaces and functions, as well as all preconnected subsets of these spaces, provided that the function is locally constant.
More concisely: If a function is locally constant on a preconnected subset of a topological space, then it is constant on that subset.
|
IsLocallyConstant.tfae
theorem IsLocallyConstant.tfae :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y),
[IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
The theorem `IsLocallyConstant.tfae` states that for any two types `X` and `Y` with `X` being a topological space and any function `f` from `X` to `Y`, the following five properties are equivalent:
1. `f` is a locally constant function, i.e., the preimage of any set under `f` is an open set.
2. For every `x` in `X`, eventually (for all `x'` in the neighborhood of `x`), `f x'` equals `f x`.
3. For every `x` in `X`, the set `{x' | f x' = f x}` is an open set.
4. For every `y` in `Y`, the preimage of `{y}` under `f` is an open set.
5. For every `x` in `X`, there exists an open set `U` containing `x` such that, for all `x'` in `U`, `f x'` equals `f x`.
In other words, these conditions are equivalent ways of characterizing a locally constant function in a topological space.
More concisely: A function between topological spaces is locally constant if and only if its preimages of open sets and the sets where it is constant are interchangeable.
|
IsLocallyConstant.desc
theorem IsLocallyConstant.desc :
∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_5} {β : Type u_6} (f : X → α) (g : α → β),
IsLocallyConstant (g ∘ f) → Function.Injective g → IsLocallyConstant f
The theorem `IsLocallyConstant.desc` states that given topological space `X` and types `α` and `β`, if a composite function `g ∘ f` (i.e., first apply `f`, then `g`), where `f : X → α` and `g : α → β`, is locally constant and `g` is an injective function, then it follows that `f` is also locally constant.
Here, a function being locally constant means that the preimage of any set under the function is an open set in the topological space. In other words, for any set in the codomain, the set of all points in the domain that map to that set is an open set. An injective function (or one-to-one function) is a function that maps distinct elements of its domain to distinct elements of its codomain; that is, `g(x) = g(y)` implies `x = y`.
More concisely: If `g ∘ f` is locally constant and `g` is injective, then `f` is locally constant.
|
LocallyConstant.coe_comap
theorem LocallyConstant.coe_comap :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(f : C(X, Y)) (g : LocallyConstant Y Z), ⇑(LocallyConstant.comap f g) = ⇑g ∘ ⇑f
This theorem states that for any types `X`, `Y`, and `Z`, given the topological spaces on `X` and `Y`, a function `f` mapping `X` to `Y`, and a locally constant function `g` from `Y` to `Z`, if `f` is a continuous function, then the co-domain mapping of the comap operation (the process of pulling back `g` along `f`) on `f` and `g` is equal to the composition of the co-domain mapping of `g` and `f`. In other words, it says that the comap operation preserves the continuous composition of functions in the context of locally constant functions.
More concisely: If `f` is a continuous function between topological spaces `X` and `Y`, and `g` is a locally constant function from `Y` to `Z`, then the co-domain mappings of `g` and the comap operation of `g` over `f` are equal, i.e., `g∘f ∘ iB(f) = iB(g)∘f`.
|
Mathlib.Topology.LocallyConstant.Basic._auxLemma.9
theorem Mathlib.Topology.LocallyConstant.Basic._auxLemma.9 : ∀ (n : ℕ), (n.succ.succ = 1) = False
This theorem, which is a part of the Mathlib.Topology.LocallyConstant.Basic module, states that for any natural number `n`, the statement that the successor of the successor of `n` is equal to 1 is always False. In other words, it's impossible for a natural number `n` increased by 2 to be equal to 1. This is a basic rule in natural number arithmetic and is true for any natural number `n`.
More concisely: The theorem asserts that for all natural numbers `n`, `n + 2 ≠ 1`.
|
IsLocallyConstant.continuous
theorem IsLocallyConstant.continuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocallyConstant f → Continuous f
The theorem `IsLocallyConstant.continuous` states that for any types `X` and `Y`, and given the topological space structure on `X` and `Y`, if function `f` from `X` to `Y` is locally constant (i.e., the preimage of any set under `f` is open), then `f` is continuous. In other words, any function `f` that satisfies the condition that the inverse image of any subset of `Y` is an open set in `X` is guaranteed to be a continuous function.
More concisely: If a function between topological spaces is locally constant, then it is continuous.
|
Mathlib.Topology.LocallyConstant.Basic._auxLemma.5
theorem Mathlib.Topology.LocallyConstant.Basic._auxLemma.5 : ∀ {α : Type u} {a b : α}, (a ∈ {b}) = (a = b)
This theorem, given any type `α` and any two elements `a` and `b` of this type, states that `a` is in the singleton set containing `b` if and only if `a` is equal to `b`. In more mathematical terms, it establishes the equivalence `$a \in \{b\} \Leftrightarrow a = b$`.
More concisely: A singleton set contains exactly one element, so the element `a` is in the singleton set `{b}` if and only if `a` is equal to `b`. In formal notation: `a ∈ {b} ↔ a = b`.
|
LocallyConstant.comap_injective
theorem LocallyConstant.comap_injective :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(f : C(X, Y)), Function.Surjective f.toFun → Function.Injective (LocallyConstant.comap f)
The theorem `LocallyConstant.comap_injective` states that for any three types `X`, `Y`, and `Z` with `X` and `Y` being topological spaces, given a function `f` from `X` to `Y` that is continuous and surjective (i.e., for every element in `Y`, there exists an element in `X` such that the function `f` maps this element of `X` to the element of `Y`), the function `LocallyConstant.comap f`, which is the precomposition of any function with `f`, is injective (i.e., if `LocallyConstant.comap f` maps two elements of its domain to the same value, then these two elements were the same to begin with).
More concisely: If `f: X → Y` is a continuous and surjective function between topological spaces `X` and `Y`, then `LocallyConstant.comap f` is an injective function.
|
IsLocallyConstant.isClopen_fiber
theorem IsLocallyConstant.isClopen_fiber :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
IsLocallyConstant f → ∀ (y : Y), IsClopen {x | f x = y}
The theorem `IsLocallyConstant.isClopen_fiber` states that for any topological spaces `X` and `Y`, and any function `f` from `X` to `Y`, if `f` is locally constant (meaning the preimage of any set is an open set), then for any element `y` from `Y`, the set of all elements `x` from `X` such that `f(x) = y` is a clopen set (meaning it is both closed and open). In mathematical terms, this is stating that the inverse image of a point under a locally constant function is always a clopen set.
More concisely: If `f: X → Y` is a locally constant function between topological spaces, then for each `y ∈ Y`, the preimage `f⁁⁻¹{y} ⊆ X` is a clopen set.
|
IsLocallyConstant.comp₂
theorem IsLocallyConstant.comp₂ :
∀ {X : Type u_1} [inst : TopologicalSpace X] {Y₁ : Type u_5} {Y₂ : Type u_6} {Z : Type u_7} {f : X → Y₁}
{g : X → Y₂},
IsLocallyConstant f → IsLocallyConstant g → ∀ (h : Y₁ → Y₂ → Z), IsLocallyConstant fun x => h (f x) (g x)
The theorem `IsLocallyConstant.comp₂` states that, given any two functions `f` and `g` from a topological space `X` to `Y₁` and `Y₂` respectively, if both `f` and `g` are locally constant then for any function `h` from `Y₁` and `Y₂` to `Z`, the function composed by `h`, `f` and `g` is also locally constant. In other words, the theorem asserts the preservation of local constancy under function composition.
More concisely: If `f` and `g` are locally constant functions from a topological space `X` to `Y₁` and `Y₂` respectively, then their composition `h ∘ f ∘ g` is also a locally constant function from `X` to `Z`, for any function `h` from `Y₁` to `Z`.
|