preimage_prodMap

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#IsSymmetricRel.preimage_prodMap

← MathLib Explorer

English

If U is symmetric, then the preimage of U under Prod.map f f is symmetric.

Русский

Если U симметрично, то предобраз под Prod.map f f симметричен.

LaTeX

$$IsSymmetricRel U → ∀ f, IsSymmetricRel (Set.preimage (Prod.map f f) U)$$

Lean4

theorem preimage_prodMap {U : Set (β × β)} (ht : IsSymmetricRel U) (f : α → β) : IsSymmetricRel (Prod.map f f ⁻¹' U) :=
  Set.ext fun _ ↦ ht.mk_mem_comm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru