mem_comp_of_mem_ball — Mathlib

English

If x ∈ ball z V and y ∈ ball z W, then (x, y) lies in the product relation V ○ W.

Русский

Если x принадлежит шару вокруг z по V и y принадлежит шару вокруг z по W, то пара (x, y) принадлежит композиции V ○ W.

LaTeX

$$$(x, y) \in V \circ W \quad\text{whenever}\quad x \in \operatorname{ball}(z, V) \text{ and } y \in \operatorname{ball}(z, W)$$$

Lean4

theorem mem_comp_of_mem_ball {V W : Set (β × β)} {x y z : β} (hV : IsSymmetricRel V) (hx : x ∈ ball z V)
    (hy : y ∈ ball z W) : (x, y) ∈ V ○ W := by
  rw [mem_ball_symmetry hV] at hx
  exact ⟨z, hx, hy⟩

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