covBy_iff_exists_insert — Mathlib

English

For sets s and t, s ⋖ t if and only if there exists a ∉ s with t = insert a s.

Русский

Для множеств s и t выполняется: s ⋖ t тогда и только тогда, когда существует a ∉ s такое, что t = insert a s.

LaTeX

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

Lean4

theorem covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t :=
  ⟨CovBy.exists_set_insert, by rintro ⟨a, ha, rfl⟩; exact covBy_insert ha⟩

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