set_cases — Mathlib

English

Assuming α is Subsingleton, if a property holds for ∅ and for univ, it holds for every subset s.

Русский

Пусть α — однопредметный тип. Если свойство выполняется для ∅ и для вселенной, то выполняется и для любого s.

LaTeX

$$$ p\\emptyset \\to p(\\mathrm{univ}) \\to \\forall s: Set \\alpha, p(s) $$$

Lean4

@[elab_as_elim]
theorem set_cases {p : Set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s :=
  (s.eq_empty_or_nonempty.elim fun h => h.symm ▸ h0) fun h => (eq_univ_of_nonempty h).symm ▸ h1

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