infEdist_inv

Mathlib.Analysis.Normed.Group.Pointwise

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

English

For a normed group M and x ∈ M, s ⊆ M, infEdist(x⁻¹, s) = infEdist(x, s⁻¹).

Русский

Для нормированной группы M и x ∈ M, множество s ⊆ M: infEdist(x⁻¹, s) = infEdist(x, s⁻¹).

LaTeX

$$$\infEdist(x^{-1}, s) = \infEdist(x, s^{-1})$$$

Lean4

@[to_additive]
theorem infEdist_inv (x : E) (s : Set E) : infEdist x⁻¹ s = infEdist x s⁻¹ := by rw [← infEdist_inv_inv, inv_inv]

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

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

Разделы

Аффилиация

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