sigmaToiUnion_surjective

Mathlib.Data.Set.Lattice

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

← MathLib Explorer

English

The map sigmaToiUnion t is surjective onto ⋃ a, t(a).

Русский

Отображение sigmaToiUnion t сурьективно на ⋃ a t(a).

LaTeX

$$$$\\text{sigmaToiUnion } t \\text{ is surjective onto } \\bigcup_a t(a). $$$$

Lean4

theorem sigmaToiUnion_surjective : Surjective (sigmaToiUnion t)
  | ⟨b, hb⟩ =>
    have : ∃ a, b ∈ t a := by simpa using hb
    let ⟨a, hb⟩ := this
    ⟨⟨a, b, hb⟩, rfl⟩

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

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

Разделы

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

Аффилиация

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