covBy_iff_exists_cons — Mathlib

English

A cover relation s ⋖ t holds if and only if there exists an element a and a proof that a ∉ s with t = s.cons a ha.

Русский

Отношение покрытия s ⋖ t эквивалентно существованию элемента a и доказательства того, что a ∉ s, при котором t = s.cons a ha.

LaTeX

$$$ s \covBy t \iff \exists a, \exists ha:\ s.cons a ha = t $$$

Lean4

theorem covBy_iff_exists_cons : s ⋖ t ↔ ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
  ⟨CovBy.exists_finset_cons, by rintro ⟨a, ha, rfl⟩; exact covBy_cons _⟩

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