subsingleton_of_subsingleton_inter_right

English

Let s and t be subsets of a set. If s ∪ t is a subsingleton, then t is a subsingleton.

Русский

Пусть s и t — подмножества. Если s ∪ t является подсинглотоном, то t является подсинглотоном.

LaTeX

$$$ \forall \alpha \; \forall s,t : \mathrm{Set}\ \alpha, \ (s \cup t).Subsingleton \rightarrow t.Subsingleton $$$

Lean4

theorem subsingleton_of_subsingleton_inter_right (h : (s ∪ t).Subsingleton) : t.Subsingleton := fun _ h₁ _ h₂ ↦
  h (.inr h₁) (.inr h₂)

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