sup_sdiff_mem_of_mem_compression_of_notMem

English

If a ∈ 𝓒 u v s and a ∉ s, then (a ⊔ v) \\ u ∈ s; i.e., a can be reconstructed by sup and sdiff operations inside s.

Русский

Если a ∈ 𝓒_{u,v}(s) и a ∉ s, то (a ∨ v) \\ u ∈ s.

LaTeX

$$(a \\lor v) \\ u ∈ s$$

Lean4

theorem sup_sdiff_mem_of_mem_compression_of_notMem (h : a ∈ 𝓒 u v s) (ha : a ∉ s) : (a ⊔ v) \ u ∈ s :=
  by
  rw [mem_compression] at h
  obtain h | ⟨-, b, hb, hba⟩ := h
  · cases ha h.1
  unfold compress at hba
  split_ifs at hba with h
  · rwa [← hba, sdiff_sup_cancel (le_sup_of_le_left h.2), sup_sdiff_right_self, h.1.symm.sdiff_eq_left]
  · cases ne_of_mem_of_not_mem hb ha hba

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