subset_sups — Mathlib

English

If a set u is contained in s ⊻ t, then there exist finite s' ⊆ s and t' ⊆ t with u ⊆ s' ⊻ t'.

Русский

Если множество u содержится в s ⊻ t, найдутся конечные s' ⊆ s и t' ⊆ t такие, что u ⊆ s' ⊻ t'.

LaTeX

$$$ u \subseteq s \oplus t \Rightarrow \exists s',t' \subseteq_F s,t' \subseteq_F t: u \subseteq s' \oplus t' $$$

Lean4

theorem subset_sups {s t : Set α} : ↑u ⊆ s ⊻ t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t' :=
  subset_set_image₂

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