LeanPool.WhiteheadTheorem.Auxiliary #

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Auxiliary.

theorem CategoryTheory.eq_of_comp_right_iso_eq {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} (h : X ⟶ Y) [IsIso h] {f g : Y ⟶ Z} (e : CategoryStruct.comp h f = CategoryStruct.comp h g) :

f = g

source

theorem CategoryTheory.eq_of_comp_left_iso_eq {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} (h : Y ⟶ Z) [IsIso h] {f g : X ⟶ Y} (e : CategoryStruct.comp f h = CategoryStruct.comp g h) :

f = g

source

instance TopCat.isIso_of_isEmpty {X Y : TopCat} [IsEmpty ↑X] [IsEmpty ↑Y] (f : X ⟶ Y) :

CategoryTheory.IsIso f

source

instance TopCat.isEmpty_sigmaObj_of_isEmpty_dom {β : Type w} (f : β → TopCat) [CategoryTheory.Limits.HasCoproduct f] [IsEmpty β] :

IsEmpty ↑(∐ f)

source

theorem ContinuousMap.eq_of_topCat_ofHom {A B : Type u} [TopologicalSpace A] [TopologicalSpace B] {f g : C(A, B)} (e : TopCat.ofHom f = TopCat.ofHom g) :

f = g

source

theorem ContinuousMap.Homotopic.of_eq (X Y : Type u) [TopologicalSpace X] [TopologicalSpace Y] (f g : C(X, Y)) (hfg : f = g) :

f.Homotopic g

Auxiliary lemmas used in largeCubeHomeoPDisk and largeCubeBoundaryHomeoPDiskBoundary

source

theorem Real.forall_le_of_iSup_le_of_bddAbove {ι : Sort u_1} {f : ι → ℝ} {a : ℝ} (hbdd : BddAbove (Set.range f)) (hf : ⨆ (i : ι), f i ≤ a) (i : ι) :

f i ≤ a

source

theorem Real.range_bddAbove_of_finite_domain {ι : Type u_1} (f : ι → ℝ) [Finite ι] :

BddAbove (Set.range f)

source

theorem Real.forall_le_of_iSup_le_of_finite_domain {ι : Type u_1} {f : ι → ℝ} {a : ℝ} [Finite ι] (hf : ⨆ (i : ι), f i ≤ a) (i : ι) :

f i ≤ a

source

theorem Real.le_iSup_of_exists_ge_of_bddAbove {ι : Sort u_1} {f : ι → ℝ} {a : ℝ} (hbdd : BddAbove (Set.range f)) (hf : ∃ (i : ι), a ≤ f i) :

a ≤ ⨆ (i : ι), f i

source

theorem Real.le_iSup_of_exists_ge_of_finite_domain {ι : Type u_1} {f : ι → ℝ} {a : ℝ} [Finite ι] (hf : ∃ (i : ι), a ≤ f i) :

a ≤ ⨆ (i : ι), f i

source

theorem Real.exists_eq_of_iSup_eq_of_finite_domain {ι : Type u_1} {f : ι → ℝ} {a : ℝ} [Finite ι] (hfz : ∃ (i : ι), f i ≥ 0) (hf : ⨆ (i : ι), f i = a) :

∃ (i : ι), f i = a

source

noncomputable def ContinuousMap.liftCoverClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_3} [Finite ι] (S : ι → Set α) (φ : (i : ι) → C(↑(S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩) (hS_cover : ∀ (x : α), ∃ (i : ι), x ∈ S i) (hS_closed : ∀ (i : ι), IsClosed (S i)) :

C(α, β)

liftCoverClosed

Equations

ContinuousMap.liftCoverClosed S φ hφ hS_cover hS_closed = { toFun := Set.liftCover S (fun (i : ι) => ⇑(φ i)) hφ ⋯, continuous_toFun := ⋯ }

Instances For

source

theorem ContinuousMap.liftCoverClosed_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_3} [Finite ι] (S : ι → Set α) (φ : (i : ι) → C(↑(S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩) (hS_cover : ∀ (x : α), ∃ (i : ι), x ∈ S i) (hS_closed : ∀ (i : ι), IsClosed (S i)) {i : ι} (x : ↑(S i)) :

(liftCoverClosed S φ hφ hS_cover hS_closed) ↑x = (φ i) x

source

theorem ContinuousMap.liftCoverClosed_coe' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_3} [Finite ι] (S : ι → Set α) (φ : (i : ι) → C(↑(S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩) (hS_cover : ∀ (x : α), ∃ (i : ι), x ∈ S i) (hS_closed : ∀ (i : ι), IsClosed (S i)) {i : ι} (x : α) (hx : x ∈ S i) :

(liftCoverClosed S φ hφ hS_cover hS_closed) x = (φ i) ⟨x, hx⟩