preimage_subset_of_surjOn

Mathlib.Data.Set.Image

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

English

If f is injective and h is SurjOn f s t, then f^{-1}(t) ⊆ s.

Русский

Если f инъективна и h = SurjOn f s t, тогда f^{-1}(t) ⊆ s.

LaTeX

$$f is injective ∧ h : SurjOn f s t ⇒ Preimage f t ⊆ s$$

Lean4

theorem preimage_subset_of_surjOn {t : Set β} (hf : Injective f) (h : SurjOn f s t) : f ⁻¹' t ⊆ s := fun _ hx ↦
  hf.mem_set_image.1 <| h hx

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

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

Разделы

Аффилиация

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