countable_of_injOn — Mathlib

English

If f is injective on s and hf' : InjOn f s, and t = f''s is countable, then s is countable.

Русский

Если f инъективно на s и t = f''s счётно, то s счётно.

LaTeX

$$$\\operatorname{MapsTo}(f,s,t) \\wedge \\operatorname{InjOn}(f,s) \\wedge \\operatorname{Countable}(t) \\Rightarrow \\operatorname{Countable}(s)$$$

Lean4

theorem countable_of_injOn {s : Set α} {t : Set β} {f : α → β} (hf : MapsTo f s t) (hf' : InjOn f s)
    (ht : t.Countable) : s.Countable :=
  have := ht.to_subtype
  have : Injective (hf.restrict f s t) := (injOn_iff_injective.1 hf').codRestrict _
  this.countable

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