sdiff_singleton_covBy — Mathlib

English

If a ∈ s, then removing a from s yields a predecessor directly below s in the subset order: s \ {a} ⋖ s.

Русский

Если a ∈ s, то удаление a из s дает предшественник прямо ниже s в порядке включения: s \ {a} ⋖ s.

LaTeX

$$$ s \ { a } ⋖ s $$$

Lean4

@[simp]
theorem sdiff_singleton_covBy (ha : a ∈ s) : s \ { a } ⋖ s :=
  ⟨sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _, (sdiff_singleton_wcovBy _ _).2⟩

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