funProp minimal setup for Continuous(At/On) #
theorem
continuousAt_id'
{α : Type u_1}
[TopologicalSpace α]
(y : α)
:
ContinuousAt (fun (x : α) => x) y
theorem
continuousOn_id'
{α : Type u_1}
[TopologicalSpace α]
(s : Set α)
:
ContinuousOn (fun (x : α) => x) s
theorem
ContinuousAt.comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace α]
{g : β → γ}
{f : α → β}
{x : α}
(hg : ContinuousAt g (f x))
(hf : ContinuousAt f x)
:
ContinuousAt (fun (x : α) => g (f x)) x
theorem
ContinuousOn.comp''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace α]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : ContinuousOn g t)
(hf : ContinuousOn f s)
(h : Set.MapsTo f s t)
:
ContinuousOn (fun (x : α) => g (f x)) s
theorem
continuousOn_apply
{ι : Type u_4}
{π : ι → Type u_5}
[T : (i : ι) → TopologicalSpace (π i)]
(i : ι)
(s : Set ((i : ι) → π i))
:
ContinuousOn (fun (p : (i : ι) → π i) => p i) s
theorem
continuousAt_pi'
{α : Type u_1}
{ι : Type u_4}
{π : ι → Type u_5}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
{x : α}
(hf : ∀ (i : ι), ContinuousAt (fun (y : α) => f y i) x)
:
ContinuousAt f x
theorem
continuousOn_pi'
{α : Type u_1}
{ι : Type u_4}
{π : ι → Type u_5}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
{s : Set α}
(hf : ∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s)
:
ContinuousOn f s
theorem
Continuous.div₀
{α : Type u_1}
{G₀ : Type u_3}
[TopologicalSpace α]
[GroupWithZero G₀]
[TopologicalSpace G₀]
[HasContinuousInv₀ G₀]
[ContinuousMul G₀]
{f : α → G₀}
{g : α → G₀}
(hf : Continuous f)
(hg : Continuous g)
(h₀ : ∀ (x : α), g x ≠ 0)
:
Continuous fun (x : α) => f x / g x
theorem
ContinuousAt.div₀
{α : Type u_1}
{G₀ : Type u_3}
[TopologicalSpace α]
[GroupWithZero G₀]
[TopologicalSpace G₀]
[HasContinuousInv₀ G₀]
[ContinuousMul G₀]
{f : α → G₀}
{g : α → G₀}
{a : α}
(hf : ContinuousAt f a)
(hg : ContinuousAt g a)
(h₀ : g a ≠ 0)
:
ContinuousAt (fun (x : α) => f x / g x) a
theorem
ContinuousOn.div₀
{α : Type u_1}
{G₀ : Type u_3}
[TopologicalSpace α]
[GroupWithZero G₀]
[TopologicalSpace G₀]
[HasContinuousInv₀ G₀]
[ContinuousMul G₀]
{f : α → G₀}
{g : α → G₀}
{s : Set α}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
(h₀ : ∀ x ∈ s, g x ≠ 0)
:
ContinuousOn (fun (x : α) => f x / g x) s