mem_ball_symmetry — Mathlib

English

If V is symmetric, then x belongs to the ball around y with V if and only if y belongs to the ball around x with V.

Русский

Если V симметрично, то x принадлежит шару вокруг y по V тогда и только тогда, когда y принадлежит шару вокруг x по V.

LaTeX

$$$x \in \operatorname{ball}(y, V) \iff y \in \operatorname{ball}(x, V)$$$

Lean4

theorem mem_ball_symmetry {V : Set (β × β)} (hV : IsSymmetricRel V) {x y} : x ∈ ball y V ↔ y ∈ ball x V :=
  show (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V by
    unfold IsSymmetricRel at hV
    rw [hV]

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