exists_finset_cons — Mathlib

English

If h: s ⋖ t, then there exists a with t = s.cons a ha for some ha.

Русский

Если h: s ⋖ t, тогда существует a, такое что t = s.cons a ha для некоторого ha.

LaTeX

$$$ h.lt \Rightarrow \exists a, \exists ha:\ a \notin s, s.cons a ha = t $$$

Lean4

theorem _root_.CovBy.exists_finset_cons (h : s ⋖ t) : ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
  let ⟨a, ha, hst⟩ := ssubset_iff_exists_cons_subset.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_cons _).symm⟩

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