compress_of_disjoint_of_le

Mathlib.Combinatorics.SetFamily.Compression.UV

URI: https://scilib.ai/kg/mathlib#UV.compress_of_disjoint_of_le

English

If u and a are disjoint and v ≤ a, then the compressed element equals (a ⊔ u) \\ v.

Русский

Если u и a непересекаются и v ≤ a, то сжатый элемент равен (a ⊔ u) \\ v.

LaTeX

$$$\\text{compress of disjoint of le}: \\mathrm{compress} \\ u\\ v\\ a = (a \\lor u) \\setminus v$$$

Lean4

theorem compress_of_disjoint_of_le (hua : Disjoint u a) (hva : v ≤ a) : compress u v a = (a ⊔ u) \ v :=
  if_pos ⟨hua, hva⟩

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

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

Разделы

Аффилиация

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