mem_of_mem_compression — Mathlib

English

If a ∈ 𝓒 u v s and v ≤ a and v = ⊥ → u = ⊥, then a ∈ s; the compressed element lies in the original set under mild conditions.

Русский

Если a ∈ 𝓒_{u,v}(s) и v ≤ a, и условие v = ⊥ → u = ⊥ выполняется, то a ∈ s.

LaTeX

$$a ∈ s$$

Lean4

/-- If `a` is in the `u, v`-compression but `v ≤ a`, then `a` must have been in the original
family. -/
theorem mem_of_mem_compression (ha : a ∈ 𝓒 u v s) (hva : v ≤ a) (hvu : v = ⊥ → u = ⊥) : a ∈ s :=
  by
  rw [mem_compression] at ha
  obtain ha | ⟨_, b, hb, h⟩ := ha
  · exact ha.1
  unfold compress at h
  split_ifs at h
  · rw [← h, le_sdiff_right] at hva
    rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
  · rwa [← h]

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