English
If a ∈ 𝓒 u v s, v ≤ a, and u ⟂ a, then (a ⊔ u) \\ v ∈ s; i.e., the compressed element back-projects into s under disjointness assumptions.
Русский
Если a ∈ 𝓒_{u,v}(s) и v ≤ a, и u ⟂ a, то (a ∨ u) \\ v ∈ s.
LaTeX
$$(a \\lor u) \\ v ∈ s$$
Lean4
/-- If `a` is in the family compression and can be compressed, then its compression is in the
original family. -/
theorem sup_sdiff_mem_of_mem_compression (ha : a ∈ 𝓒 u v s) (hva : v ≤ a) (hua : Disjoint u a) : (a ⊔ u) \ v ∈ s :=
by
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
· exact ha
have hu : u = ⊥ :=
by
suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
refine hua.mono_right ?_
rw [← compress_idem, compress_of_disjoint_of_le hua hva]
exact sdiff_le_sdiff_right le_sup_right
have hv : v = ⊥ := by
rw [← disjoint_self]
apply Disjoint.mono_right hva
rw [← compress_idem, compress_of_disjoint_of_le hua hva]
exact disjoint_sdiff_self_right
rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
