prod_subset_comm

Mathlib.Topology.UniformSpace.Defs

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

← MathLib Explorer

English

For a symmetric s, t ×ˢ u ⊆ s ⇔ u ×ˢ t ⊆ s.

Русский

Для симметричного s: t ×ˢ u ⊆ s эквивалентно u ×ˢ t ⊆ s.

LaTeX

$$$t \timesˢ u \subseteq s \iff u \timesˢ t \subseteq s$$$

Lean4

theorem prod_subset_comm {s : Set (α × α)} {t u : Set α} (hs : IsSymmetricRel s) : t ×ˢ u ⊆ s ↔ u ×ˢ t ⊆ s := by
  rw [← hs.eq, ← image_subset_iff, image_swap_prod, hs.eq]

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

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

Разделы

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

Аффилиация

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