subset_symmetrize

Mathlib.Data.Rel

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

English

S ⊆ R.symmetrize iff S ⊆ R and S ⊆ R^{-1}.

Русский

S ⊆ R.symmetrize тогда и только тогда, когда S ⊆ R и S ⊆ R^{-1}.

LaTeX

$$S ⊆ R.symmetrize ⟺ (S ⊆ R ∧ S ⊆ R^{-1})$$

Lean4

theorem subset_symmetrize {S : SetRel α α} : S ⊆ R.symmetrize ↔ S ⊆ R ∧ S ⊆ R.inv :=
  Set.subset_inter_iff

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

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

Разделы

Аффилиация

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