Mathlib Map

Theorems · Theorem · computer science

Language.add_iSup

∀ {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α), m + ⨆ i, l i = ⨆ i, m + l i
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 125Languagesup_iSup · cited by 2sup_iSupLanguage.add_iSupCITED 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
  • sup_iSupproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.