cancel_right

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.EqOn.cancel_right

← MathLib Explorer

English

If f maps s onto t, then for any g, SurjOn (g ∘ f) on s to g''t.

Русский

Если f отображает s на t, то для любого g SurjOn (g∘f) на s в g''t.

LaTeX

$$$ \mathrm{SurjOn} f s t \rightarrow \mathrm{SurjOn}(g\circ f) s (g''t) $$$

Lean4

theorem cancel_right (hf : s.EqOn (g₁ ∘ f) (g₂ ∘ f)) (hf' : s.SurjOn f t) : t.EqOn g₁ g₂ :=
  by
  intro b hb
  obtain ⟨a, ha, rfl⟩ := hf' hb
  exact hf ha

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

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

Разделы

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

Аффилиация

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