image2_right — Mathlib

English

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

Русский

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

LaTeX

$$$ t.Infinite \land a \in s \land InjOn (f a) t \Rightarrow (image2 f s t).Infinite $$$

Lean4

protected theorem image2_right (ht : t.Infinite) (ha : a ∈ s) (hf : InjOn (f a) t) : (image2 f s t).Infinite :=
  (ht.image hf).mono <| image_subset_image2_right ha

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