compress_disjoint — Mathlib

English

The two parts arising from compression are disjoint: the set of elements of s that stay in s after compression is disjoint from the image under compression of elements not in s.

Русский

Два множества, полученных из сжатия: элементы s, остающиеся в s после сжатия, и изображение элементов вне s, неподобны и не пересекаются.

LaTeX

$$$\\text{Disjoint}\\left(\\{a\\in s \\,|\\, \\mathcal{C}_{u,v}(a)\\in s\\},\\{a\\in s\\!\\cdot\\!\\text{image}(\\mathcal{C}_{u,v})\\,|\\, a\\notin s\\}\\right)$$$

Lean4

theorem compress_disjoint : Disjoint ({a ∈ s | compress u v a ∈ s}) ({a ∈ s.image <| compress u v | a ∉ s}) :=
  disjoint_left.2 fun _a ha₁ ha₂ ↦ (mem_filter.1 ha₂).2 (mem_filter.1 ha₁).1

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