mk_preimage_of_subset_range_lift

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_preimage_of_subset_range_lift

← MathLib Explorer

English

If s ⊆ range f, then |s| ≤ |f^{-1}(s)| after lifting.

Русский

Если s ⊆ образ f, то |s| ≤ |f^{-1}(s)| после подъёма.

LaTeX

$$$|s| \\le |f^{-1}(s)|$$$

Lean4

theorem mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : s ⊆ range f) :
    lift.{u} #s ≤ lift.{v} #(f ⁻¹' s) := by
  rw [← image_preimage_eq_iff] at h
  nth_rewrite 1 [← h]
  apply mk_image_le_lift

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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