preimage

Mathlib.Data.Set.Countable

URI: https://scilib.ai/kg/mathlib#Set.Countable.preimage

English

If s is countable and f is injective, then f^{-1}(s) is countable.

Русский

Если s счетно и f инъективна, то f^{-1}(s) счетно.

LaTeX

$$$\\operatorname{Countable}(s) \\Rightarrow \\operatorname{Countable}(f^{-1}(s))$ при $\\operatorname{Injective}(f)$$$

Lean4

protected theorem preimage {s : Set β} (hs : s.Countable) {f : α → β} (hf : Injective f) : (f ⁻¹' s).Countable :=
  hs.preimage_of_injOn hf.injOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru