This file defined a bundled type for well-defined properties of topological spaces.

structure PiBase.Formal.Property : Type (u + 1)

Formally, we use the Property structure to encode properties of topological functions, which consist of the property in question and a proof that it is being preserved under homeomorphism.

• toPred (X : Type u) [TopologicalSpace X] : Prop
• well_defined {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (h : self.toPred X) : self.toPred Y

@[instance_reducible]

instance PiBase.Formal.Property.instDFunLikeTypeForallTopologicalSpaceProp : DFunLike Property (Type u) fun (X : Type u) => [TopologicalSpace X] → Prop

Equations

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

@[reducible, inline]

abbrev PiBase.Formal.WellDefined.toProperty {P : (X : Type u) → TopologicalSpace X → Prop} (h : WellDefined P) : Property

Equations

• PiBase.Formal.WellDefined.toProperty h = { toPred := fun (X : Type ?u.1) (t : TopologicalSpace X) => P X t, well_defined := ⋯ }

theorem PiBase.Formal.Property.toPred_injective : Function.Injective toPred

theorem PiBase.Formal.Property.well_defined_of_property (p : Property) {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) : p X ↔ p Y

For two homeomorphic spaces X, Y, if p of type Property , p X and p Y are equivalent.