symmetrize_mono

Mathlib.Data.Rel

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

English

If R1 ⊆ R2, then R1.symmetrize ⊆ R2.symmetrize.

Русский

Если R1 ⊆ R2, то R1.symmetrize ⊆ R2.symmetrize.

LaTeX

$$R1.symmetrize ⊆ R2.symmetrize$$

Lean4

@[gcongr]
theorem symmetrize_mono (h : R₁ ⊆ R₂) : R₁.symmetrize ⊆ R₂.symmetrize :=
  Set.inter_subset_inter h <| Set.preimage_mono h

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

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

Разделы

Аффилиация

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