inter

Mathlib.Topology.UniformSpace.Defs

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

← MathLib Explorer

English

Intersection of symmetric relations is symmetric: IsSymmetricRel (U ∩ V).

Русский

Пересечение симметричных отношений симметрично: IsSymmetricRel (U ∩ V).

LaTeX

$$IsSymmetricRel (U \cap V)$$

Lean4

theorem inter {U V : Set (α × α)} (hU : IsSymmetricRel U) (hV : IsSymmetricRel V) : IsSymmetricRel (U ∩ V) := by
  rw [IsSymmetricRel, preimage_inter, hU.eq, hV.eq]

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

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

Разделы

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

Аффилиация

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