homothety_continuous

Mathlib.Topology.Algebra.Affine

URI: https://scilib.ai/kg/mathlib#AffineMap.homothety_continuous

English

For any center x in P and scalar t, the homothety map homothety(x,t) is continuous.

Русский

Для любого центра x в P и скаляра t отображение гомотетии homothety(x,t) непрерывно.

LaTeX

$$$\text{Continuous}(homothety(x,t))$$$

Lean4

@[continuity, fun_prop]
theorem homothety_continuous (x : P) (t : R) : Continuous <| homothety x t :=
  by
  rw [coe_homothety]
  fun_prop

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru