covBy_iff_exists_insert — Mathlib

English

Let s and t be Finsetα. Then s is covered by t in the Finset order (i.e., t covers s) if and only if there exists an element a not in s such that t = insert a s.

Русский

Пусть s и t — конечные множества Finsetα. Тогда t покрывает s в порядке включения тогда и только тогда существует элемент a, которого нет в s, и t получается добавлением a к s: t = insert a s.

LaTeX

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

Lean4

theorem covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := by
  simp only [← coe_covBy_coe, Set.covBy_iff_exists_insert, ← coe_inj, coe_insert, mem_coe]

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