ball_subset_of_mem — Mathlib

English

If V is transitive, and y ∈ ball x V, then ball y V ⊆ ball x V.

Русский

Если V транзитивно и y лежит в шаре вокруг x, то шар вокруг y содержится в шаре вокруг x.

LaTeX

$$$\text{Transitive}(V) \Rightarrow y \in \mathrm{ball}(x,V) \Rightarrow \mathrm{ball}(y,V) \subseteq \mathrm{ball}(x,V)$$$

Lean4

theorem ball_subset_of_mem {V : Set (X × X)} (h : IsTransitiveRel V) {x y : X} (hy : y ∈ ball x V) :
    ball y V ⊆ ball x V :=
  ball_subset_of_comp_subset hy (h.comp_subset_self)

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