disjoint_of_mem_compression_of_notMem

English

If a ∈ 𝓒 u v s and a ∉ s, then Disjoint v a.

Русский

Если a ∈ 𝓒_{u,v}(s) и a ∉ s, тогда v и a несмежны.

LaTeX

$$a ∈ 𝓒_{u,v}(s) ∧ a ∉ s ⇒ Disjoint(v,a)$$

Lean4

theorem disjoint_of_mem_compression_of_notMem (h : a ∈ 𝓒 u v s) (ha : a ∉ s) : Disjoint v a :=
  by
  rw [mem_compression] at h
  obtain h | ⟨-, b, hb, hba⟩ := h
  · cases ha h.1
  unfold compress at hba
  split_ifs at hba
  · rw [← hba]
    exact disjoint_sdiff_self_right
  · cases ne_of_mem_of_not_mem hb ha hba

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