le_of_mem_compression_of_notMem — Mathlib

English

If a ∈ 𝓒 u v s and a ∉ s then a is disjoint from v; i.e., v ⟂ a.

Русский

Если a ∈ 𝓒_{u,v}(s) и a ∉ s, то a несмежен с v; то есть v ∧ a = 0.

LaTeX

$$If a ∈ 𝓒_{u,v}(s) and a ∉ s then Disjoint(v,a).$$

Lean4

theorem le_of_mem_compression_of_notMem (h : a ∈ 𝓒 u v s) (ha : a ∉ s) : u ≤ 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 with h
  · rw [← hba, le_sdiff]
    exact ⟨le_sup_right, h.1.mono_right h.2⟩
  · cases ne_of_mem_of_not_mem hb ha hba

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