image2_left — Mathlib

English

If s is infinite, b ∈ t, and f(·, b) is injective on s, then image2 f s t is infinite.

Русский

Если s бесконечно, b ∈ t и f(·, b) инъективна на s, то image2 f s t бесконечно.

LaTeX

$$$ s.Infinite \land b \in t \land InjOn (fun a => f a b) s \Rightarrow (image2 f s t).Infinite $$$

Lean4

protected theorem image2_left (hs : s.Infinite) (hb : b ∈ t) (hf : InjOn (fun a => f a b) s) :
    (image2 f s t).Infinite :=
  (hs.image hf).mono <| image_subset_image2_left hb

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