exists_set_insert — Mathlib

English

If s is covered by t, then there exists an element a not in s such that t is obtained by inserting a into s.

Русский

Если s покрыто t, существует элемент a, не принадлежащий s, такой что t получается вставкой a в s.

LaTeX

$$$ \operatorname{CovBy}(s,t) \Rightarrow \exists a \notin s,\; \operatorname{insert}(a,s)=t $$$

Lean4

theorem _root_.CovBy.exists_set_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t :=
  let ⟨a, ha, hst⟩ := ssubset_iff_insert.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_insert ha).symm⟩

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