nonempty_of_nonempty_preimage

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.nonempty_of_nonempty_preimage

English

If the preimage f^{-1}(s) is nonempty, then s is nonempty.

Русский

Если предобраз f^{-1}(s) непуст, значит и s непуст.

LaTeX

$$(f^{-1}(s)).Nonempty → s.Nonempty$$

Lean4

theorem nonempty_of_nonempty_preimage {s : Set β} {f : α → β} (hf : (f ⁻¹' s).Nonempty) : s.Nonempty :=
  let ⟨x, hx⟩ := hf
  ⟨f x, hx⟩

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

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

Разделы

Аффилиация

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