subset_infs — Mathlib

English

If a finite 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

$$$ \uparrow u \subseteq s \⊼ t \Rightarrow \exists s', t' : Finset α, \uparrow s' \subseteq s \land \uparrow t' \subseteq t \land u \subseteq s' \⊼ t' $$$

Lean4

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

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