wcovBy_insert — Mathlib

English

If x is added to a set s, then s is weakly covered by insert x s.

Русский

Если добавить элемент x в множество s, то s с точки зрения мощности покрывает insert x s.

LaTeX

$$s \mathrm{WCovBy} \mathrm{insert}\ x\ s$$

Lean4

@[simp]
theorem wcovBy_insert (x : α) (s : Set α) : s ⩿ insert x s :=
  by
  refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_
  by_cases h : x ∈ t
  · exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)
  · refine Or.inl (subset_antisymm ?_ hst)
    rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]

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