mem_sUnion_of_mem — Mathlib

English

Let α be a type. If x belongs to a set t and t is one of the sets in a collection S of subsets of α, then x belongs to the union of S.

Русский

Пусть α — множество. Если x принадлежит множеству t и t ∈ S, где S — множество подмножеств α, то x принадлежит объединению S.

LaTeX

$$$ x \in t \land t \in S \Rightarrow x \in \bigcup S $$$

Lean4

theorem mem_sUnion_of_mem {x : α} {t : Set α} {S : Set (Set α)} (hx : x ∈ t) (ht : t ∈ S) : x ∈ ⋃₀ S :=
  ⟨t, ht, hx⟩
    -- is this theorem really necessary?

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