symmetrize_mono

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#symmetrize_mono

English

If V ⊆ W, then symmetrizeRel(V) ⊆ symmetrizeRel(W).

Русский

Если V ⊆ W, то symmetrizeRel(V) ⊆ symmetrizeRel(W).

LaTeX

$$$V \subseteq W \Rightarrow \mathrm{symmetrizeRel}(V) \subseteq \mathrm{symmetrizeRel}(W)$$$

Lean4

@[mono]
theorem symmetrize_mono {V W : Set (α × α)} (h : V ⊆ W) : symmetrizeRel V ⊆ symmetrizeRel W :=
  inter_subset_inter h <| preimage_mono h

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

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

Разделы

Аффилиация

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