range_diff_image_subset

Mathlib.Data.Set.Image

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

English

For any f and s, range f \\ f '' s ⊆ f '' sᶜ.

Русский

Для любой функции f и множества s: range f \ f '' s ⊆ f '' sᶜ.

LaTeX

$$$$ \\operatorname{range}(f) \\ \\operatorname{sdiff}(f'' s) ⊆ f'' s^{c} $$$$

Lean4

theorem range_diff_image_subset (f : α → β) (s : Set α) : range f \ f '' s ⊆ f '' sᶜ := fun _ ⟨⟨x, h₁⟩, h₂⟩ =>
  ⟨x, fun h => h₂ ⟨x, h, h₁⟩, h₁⟩

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

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

Разделы

Аффилиация

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