subset_diffs — Mathlib

English

If a finite set u is contained in the SDiff image Set.image2 (· \\ ·) s t, then there exist finite s', t' with s' ⊆ s, t' ⊆ t and u ⊆ s' \\ t'.

Русский

Если множество u находится внутри образа SDiff через s и t, то существуют подмножества s', t' такие, что s' ⊆ s, t' ⊆ t и u ⊆ s' \\ t'.

LaTeX

$$$ \\uparrow u \\subseteq \\mathrm{Set.image2}(\\backslash)(s,t) \\Rightarrow \\exists s',t'\\, (↑s' \\subseteq s) \\wedge (↑t' \\subseteq t) \\wedge (u \\subseteq s' \\setminus t') $$$

Lean4

theorem subset_diffs {s t : Set α} :
    ↑u ⊆ Set.image2 (· \ ·) s t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' \\ t' :=
  subset_set_image₂

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