exists_set_sdiff_singleton — Mathlib

English

If s is covered by t, there exists an element a in t such that t \ {a} = s.

Русский

Если s покрыто t, существует элемент a ∈ t such that t \ {a} = s.

LaTeX

$$$ s \covBy t \Rightarrow \exists a \in t,\; t \setminus \{a\} = s $$$

Lean4

theorem _root_.CovBy.exists_set_sdiff_singleton (h : s ⋖ t) : ∃ a ∈ t, t \ { a } = s :=
  let ⟨a, ha, hst⟩ := ssubset_iff_sdiff_singleton.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssubset fun h' ↦ h.2 h' <| sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _).symm⟩

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