ball_eq_of_symmetry — Mathlib

English

If V is symmetric, then the ball around x with V equals the set of y with (y, x) in V.

Русский

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

LaTeX

$$$\operatorname{ball}(x, V) = \{ y \mid (y, x) \in V \}$ \text{ if } V \text{ is symmetric}$$$

Lean4

theorem ball_eq_of_symmetry {V : Set (β × β)} (hV : IsSymmetricRel V) {x} : ball x V = {y | (y, x) ∈ V} :=
  by
  ext y
  rw [mem_ball_symmetry hV]
  exact Iff.rfl

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