surjOn_sUnion

Mathlib.Data.Set.Lattice.Image

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

English

Duplicate of previous: directed union preserves injectivity pointwise.

Русский

Дубликат: направленное объединение сохраняет инъективность по точкам.

LaTeX

$$$\\text{InjOn}(f, \\bigcup_i s_i)$ with hypotheses as above.$$

Lean4

theorem surjOn_sUnion {s : Set α} {T : Set (Set β)} {f : α → β} (H : ∀ t ∈ T, SurjOn f s t) : SurjOn f s (⋃₀ T) :=
  fun _ ⟨t, ht, hx⟩ => H t ht hx

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

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

Разделы

Аффилиация

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