ball_eq_of_mem_of_isSymmetricRel_of_isTransitiveRel

English

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

Русский

Если V симметрично и транзитивно, и y ∈ ball x V, то ball x V = ball y V.

LaTeX

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

Lean4

theorem ball_eq_of_mem_of_isSymmetricRel_of_isTransitiveRel {V : Set (X × X)} (h_symm : IsSymmetricRel V)
    (h_trans : IsTransitiveRel V) {x y : X} (hy : y ∈ ball x V) : ball x V = ball y V :=
  by
  refine le_antisymm (h_trans.ball_subset_of_mem ?_) (h_trans.ball_subset_of_mem hy)
  rwa [← mem_ball_symmetry h_symm]

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