mem_of_subsingleton — Mathlib

English

If A is a Subsingleton and S is a SetLike F A with a Nonempty witness, then every a ∈ A belongs to S.

Русский

Если A — подсупертип (Subsingleton) и S — множество структур SetLike на A с ненулевым элементом, то любой a ∈ A принадлежит S.

LaTeX

$$$ \forall a : A, a \in S. $$$

Lean4

@[nontriviality]
theorem mem_of_subsingleton {A F} [Subsingleton A] [SetLike F A] (S : F) [h : Nonempty S] {a : A} : a ∈ S :=
  by
  obtain ⟨s, hs⟩ := nonempty_subtype.mp h
  simpa [Subsingleton.elim a s]

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