α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) = ωSup (Chain.map (approxChain f) f)
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Part.fix ↑f = ↑f (Part.fix ↑f)
rw [fix_eq_ωSup f, hc]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) ≤ ωSup (Chain.map (approxChain f) f)

case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (Chain.map (approxChain f) f) ≤ ωSup (approxChain f)
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) = ωSup (Chain.map (approxChain f) f)
apply le_antisymm
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ approxChain f ≤ Chain.map (approxChain f) f
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) ≤ ωSup (Chain.map (approxChain f) f)
apply ωSup_le_ωSup_of_le _
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) j
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ approxChain f ≤ Chain.map (approxChain f) f
intro i
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) i
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) j
exists i
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
x : α✝
⊢ ↑(approxChain f) i x ≤ ↑(Chain.map (approxChain f) f) i x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) i
intro x
no goals
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
x : α✝
⊢ ↑(approxChain f) i x ≤ ↑(Chain.map (approxChain f) f) i x
apply le_f_of_mem_approx _ ⟨i, rfl⟩
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Chain.map (approxChain f) f ≤ approxChain f
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (Chain.map (approxChain f) f) ≤ ωSup (approxChain f)
apply ωSup_le_ωSup_of_le _
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(Chain.map (approxChain f) f) i ≤ ↑(approxChain f) j
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Chain.map (approxChain f) f ≤ approxChain f
intro i
no goals
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.14701
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(Chain.map (approxChain f) f) i ≤ ↑(approxChain f) j
exists i.succ