def TopologicalSpace.DirectLimit.Rel {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) (f : (i j : ι) → i ≤ j → X i → X j) : (i : ι) × X i → (i : ι) × X i → Prop

def TopologicalSpace.DirectLimit.directLimitSetoid {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) (f : (i j : ι) → i ≤ j → X i → X j) : Setoid ((i : ι) × X i)

@[reducible, inline]

abbrev TopologicalSpace.DirectLimit.Space {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (f : (i j : ι) → i ≤ j → X i → X j) : Type (max u_2 u_1)

def TopologicalSpace.DirectLimit.of {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (f : (i j : ι) → i ≤ j → X i → X j) (i : ι) (x : X i) : Space X f

theorem TopologicalSpace.DirectLimit.of_continuous {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (f : (i j : ι) → i ≤ j → X i → X j) (i : ι) : Continuous (of X f i)

theorem TopologicalSpace.DirectLimit.of_comp {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (f : (i j : ι) → i ≤ j → X i → X j) {i j : ι} (h : i ≤ j) (x : X i) : of X f j (f i j h x) = of X f i x

noncomputable def TopologicalSpace.DirectLimit.lift {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (f : (i j : ι) → i ≤ j → X i → X j) {Y : Type u_3} [TopologicalSpace Y] (ψ : (i : ι) → X i → Y) (hψ_comp : ∀ (i j : ι) (h : i ≤ j) (x : X i), ψ j (f i j h x) = ψ i x) : Space X f → Y

theorem TopologicalSpace.DirectLimit.lift_continuous {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (f : (i j : ι) → i ≤ j → X i → X j) {Y : Type u_3} [TopologicalSpace Y] (ψ : (i : ι) → X i → Y) (hψ_cont : ∀ (i : ι), Continuous (ψ i)) (hψ_comp : ∀ (i j : ι) (h : i ≤ j) (x : X i), ψ j (f i j h x) = ψ i x) : Continuous (lift X f ψ hψ_comp)