subsingleton_of_subsingleton_inter_left

English

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

Русский

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

LaTeX

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

Lean4

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

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