X Y : Compactum
f : X ⟶ Y
⊢ ∀ (x : X.A) (g : Ultrafilter X.A), ↑g ≤ 𝓝 x → Tendsto f.f (↑g) (𝓝 (Monad.Algebra.Hom.f f x))
X Y : Compactum
f : X ⟶ Y
⊢ Continuous f.f
rw [continuous_iff_ultrafilter]
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto f.f (↑g) (𝓝 (Monad.Algebra.Hom.f f x))
X Y : Compactum
f : X ⟶ Y
⊢ ∀ (x : X.A) (g : Ultrafilter X.A), ↑g ≤ 𝓝 x → Tendsto f.f (↑g) (𝓝 (Monad.Algebra.Hom.f f x))
intro x g h
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map f.f g) ≤ 𝓝 (Monad.Algebra.Hom.f f x)
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto f.f (↑g) (𝓝 (Monad.Algebra.Hom.f f x))
rw [Tendsto, ← coe_map]
case a
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ str Y (Ultrafilter.map f.f g) = Monad.Algebra.Hom.f f x
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map f.f g) ≤ 𝓝 (Monad.Algebra.Hom.f f x)
apply le_nhds_of_str_eq
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑g ≤ 𝓝 x
case a
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ str Y (Ultrafilter.map f.f g) = Monad.Algebra.Hom.f f x
rw [← str_hom_commute, str_eq_of_le_nhds _ x _]
no goals
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑g ≤ 𝓝 x
apply h