DiscreteQuotient.isClopen_preimage
theorem DiscreteQuotient.isClopen_preimage :
∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)),
IsClopen (S.proj ⁻¹' A)
This theorem states that given a type `X` equipped with a topological structure, a discrete quotient `S` of `X`, and a set `A` of elements in the quotient space under the equivalence relation defined by `S`, the preimage of `A` under the projection map from `X` to the quotient space, as implemented by `DiscreteQuotient.proj S`, is a clopen set. This means that this preimage is both a closed and open set in the topology of `X`.
More concisely: Given a topological space `(X,τ)`, a discrete quotient `S` of `X`, and a set `A` in the quotient space `S/ⓝ` under the equivalence relation `ⓝ`, the preimage `(∘π_1∘inverse∘CHeadle_Quotient.core.coe)''(A)` is a clopen set in the topology `τ` on `X`, where `π_1 : X → S/ⓝ` is the quotient map.
|
DiscreteQuotient.fiber_eq
theorem DiscreteQuotient.fiber_eq :
∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x : X),
S.proj ⁻¹' {S.proj x} = setOf (S.Rel x)
The theorem `DiscreteQuotient.fiber_eq` states that for any type `X` equipped with a topological space instance, any `DiscreteQuotient S` of `X`, and any element `x` of `X`, the preimage of the set `{DiscreteQuotient.proj S x}` under the projection `DiscreteQuotient.proj S` equals the set of all elements which are related to `x` under the equivalence relation `S.toSetoid`. In other words, this theorem says that the preimage of the equivalence class of `x` under the quotient map is exactly the set of all elements equivalent to `x`.
More concisely: For any topological space `X` and equivalence relation `S` on `X`, the preimage of the equivalence class of an element `x` in `X` under the quotient map is equal to the set of all elements related to `x` by `S`.
|
DiscreteQuotient.proj_surjective
theorem DiscreteQuotient.proj_surjective :
∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), Function.Surjective S.proj
The theorem `DiscreteQuotient.proj_surjective` states that for all types `X` equipped with a topological space structure, and for any discrete quotient `S` of `X`, the projection function from `X` to the given discrete quotient `S` is surjective. In other words, for every element in the discrete quotient `S`, there exists at least one element in `X` such that when the projection function is applied to this element, we obtain the given element in the discrete quotient.
More concisely: For any topological space X and a discrete quotient S of X, the projection function from X to S is surjective.
|
DiscreteQuotient.isOpen_setOf_rel
theorem DiscreteQuotient.isOpen_setOf_rel :
∀ {X : Type u_5} [inst : TopologicalSpace X] (self : DiscreteQuotient X) (x : X), IsOpen (setOf (self.Rel x)) := by
sorry
The theorem `DiscreteQuotient.isOpen_setOf_rel` states that for any topological space `X` and any point `x` in `X`, if `self` is a discrete quotient structure on `X`, then the set of all points `y` such that `Rel x y` holds (where `Rel` is the relation defined in the discrete quotient structure) forms an open set in the topological space `X`. In other words, the image of any point under the relation `Rel` in a discrete quotient structure is an open set.
More concisely: In a discrete quotient structure on a topological space, the set of points related to a given point forms an open set.
|