Mathlib Map

Theorems · Theorem · computer science

Language.iSup_add

∀ {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α), (⨆ i, l i) + m = ⨆ i, l i + m
Defined in
Mathlib.Computability.Language
Cited by
0 results in Mathlib
Foundations
Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Nonempty
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

iSup · cited by 2415iSupLanguage · cited by 125LanguageiSup_sup · cited by 3iSup_supLanguage.iSup_addCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • iSupstatement · cited by 2,415
  • Languagestatement and proof · cited by 125
  • iSup_supproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.