preimage_embedding

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.preimage_embedding

English

If f is an embedding, then the preimage of a finite set is finite.

Русский

Если f — вложение, то прообраз конечного множества конечен.

LaTeX

$$$\mathrm{preimage} (\mathrm{Embedding}\; f; s) \text{ finite}$$$

Lean4

theorem preimage_embedding {s : Set β} (f : α ↪ β) (h : s.Finite) : (f ⁻¹' s).Finite :=
  h.preimage fun _ _ _ _ h' => f.injective h'

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

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

Разделы

Аффилиация

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