dist_anti_right_pi

Mathlib.Analysis.Normed.Order.UpperLower

URI: https://scilib.ai/kg/mathlib#dist_anti_right_pi

English

Analogous to the left version, the right-argument distance is antitone with respect to the right component.

Русский

Аналогично левой версии, правая компонента делает расстояние антитоничным.

LaTeX

$$$\text{AntitoneOn } (\mathrm{dist} \; x) \; (\mathrm{Iic} \; x)$$$

Lean4

theorem dist_anti_right_pi : AntitoneOn (dist x) (Iic x) := by simpa only [dist_comm] using dist_anti_left_pi (y := x)

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

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

Разделы

Аффилиация

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