kdrag.theories.real.cont

Continuity and limit lemmas for real functions.

Prove pointwise closure first, then derive global continuity and limit rules.

Theorem	Statement
`real.cont.cont_at_add`	`∀f g : ℝ → ℝ, p : ℝ, cont_at(f, p) → cont_at(g, p) → cont_at(f + g, p)`
`real.cont.cont_at_mul`	`∀f g : ℝ → ℝ, p : ℝ, cont_at(f, p) → cont_at(g, p) → cont_at(f * g, p)`
`real.cont.cont_at_of_is_cont`	`∀f : ℝ → ℝ, x : ℝ, is_cont(f) → cont_at(f, x)`
`real.cont.cont_at_update_of_has_lim_at`	`∀f : ℝ → ℝ, p L : ℝ, has_lim_at(f, p, L) → cont_at(store(f, p, L), p)`
`real.cont.continuous_abs`	`is_cont(λx : ℝ, \|x\|)`
`real.cont.continuous_add_const`	`∀a₀ : ℝ, is_cont(λx : ℝ, x + a₀)`
`real.cont.continuous_at_abs`	`∀p₀ : ℝ, cont_at(λx : ℝ, \|x\|, p₀)`
`real.cont.continuous_at_add_const`	`∀a₀ p₀ : ℝ, cont_at(λx : ℝ, x + a₀, p₀)`
`real.cont.continuous_at_const`	`∀a₀ p₀ : ℝ, cont_at(λx : ℝ, a₀, p₀)`
`real.cont.continuous_at_cube`	`∀p₀ : ℝ, cont_at(λx : ℝ, x * x * x, p₀)`
`real.cont.continuous_at_id`	`∀p₀ : ℝ, cont_at(λx : ℝ, x, p₀)`
`real.cont.continuous_at_sq`	`∀p₀ : ℝ, cont_at(λx : ℝ, x * x, p₀)`
`real.cont.continuous_const`	`∀a₀ : ℝ, is_cont(λx : ℝ, a₀)`
`real.cont.continuous_cube`	`is_cont(λx : ℝ, x * x * x)`
`real.cont.continuous_id`	`is_cont(λx : ℝ, x)`
`real.cont.continuous_sq`	`is_cont(λx : ℝ, x * x)`
`real.cont.has_lim_at_abs`	`∀p₀ : ℝ, has_lim_at(λx : ℝ, \|x\|, p₀, (λx : ℝ, \|x\|)[p₀])`
`real.cont.has_lim_at_add`	`∀f g : ℝ → ℝ, p L M : ℝ, has_lim_at(f, p, L) → has_lim_at(g, p, M) → has_lim_at(f + g, p, L + M)`
`real.cont.has_lim_at_add_const`	`∀a₀ p₀ : ℝ, has_lim_at(λx : ℝ, x + a₀, p₀, (λx : ℝ, x + a₀)[p₀])`
`real.cont.has_lim_at_const`	`∀a₀ p₀ : ℝ, has_lim_at(λx : ℝ, a₀, p₀, (λx : ℝ, a₀)[p₀])`
`real.cont.has_lim_at_cube`	`∀p₀ : ℝ, has_lim_at(λx : ℝ, x * x * x, p₀, (λx : ℝ, x * x * x)[p₀])`
`real.cont.has_lim_at_id`	`∀p₀ : ℝ, has_lim_at(λx : ℝ, x, p₀, (λx : ℝ, x)[p₀])`
`real.cont.has_lim_at_mul`	`∀f g : ℝ → ℝ, p L M : ℝ, has_lim_at(f, p, L) → has_lim_at(g, p, M) → has_lim_at(f * g, p, L * M)`
`real.cont.has_lim_at_of_cont_at`	`∀f : ℝ → ℝ, x : ℝ, cont_at(f, x) → has_lim_at(f, x, f[x])`
`real.cont.has_lim_at_of_cont_at_update`	`∀f : ℝ → ℝ, p L : ℝ, cont_at(store(f, p, L), p) → has_lim_at(f, p, L)`
`real.cont.has_lim_at_sq`	`∀p₀ : ℝ, has_lim_at(λx : ℝ, x * x, p₀, (λx : ℝ, x * x)[p₀])`
`real.cont.is_cont_add`	`∀f g : ℝ → ℝ, is_cont(f) → is_cont(g) → is_cont(f + g)`
`real.cont.is_cont_mul`	`∀f g : ℝ → ℝ, is_cont(f) → is_cont(g) → is_cont(f * g)`