ball_entourageProd — Mathlib

English

If u and v are symmetric relations, then entourageProd u v is symmetric.

Русский

Если u и v симметричны, то entourageProd u v симметрично.

LaTeX

$$$IsSymmetricRel(u) \to IsSymmetricRel(v) \to IsSymmetricRel(entourageProd(u,v))$$$

Lean4

theorem ball_entourageProd (u : Set (α × α)) (v : Set (β × β)) (x : α × β) :
    ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v := by ext p;
  simp only [ball, entourageProd, Set.mem_setOf_eq, Set.mem_prod, Set.mem_preimage]

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