inter_empty_of_inter_sUnion_empty

English

Let S be a collection of subsets of α, and s,t ⊆ α with t ∈ S. If s ∩ ⋃₀ S = ∅, then s ∩ t = ∅.

Русский

Пусть S — множество подмножеств α, а s,t ⊆ α и t ∈ S. Если s ∩ ⋃₀ S = ∅, то s ∩ t = ∅.

LaTeX

$$$$ t \\in S \\quad \\wedge\\quad s \\cap \\bigcup S = \\emptyset \\quad \\Rightarrow\\quad s \\cap t = \\emptyset. $$$$

Lean4

theorem inter_empty_of_inter_sUnion_empty {s t : Set α} {S : Set (Set α)} (hs : t ∈ S) (h : s ∩ ⋃₀ S = ∅) : s ∩ t = ∅ :=
  eq_empty_of_subset_empty <| by rw [← h]; exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

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