English
The dependent sum type Σˣ f is introduced as an alias for the disjoint sum over the index set, parameterized by the embedding data f.
Русский
Задается зависимая сумма Σˣ f как псевдоним для дизъюнктивного объединения по индексу, с учётом данных вложений f.
LaTeX
$$${\\Sigma}^\\bullet f := \\sum_{i\\in ι} G_i$$$
Lean4
/-- Alias for `Σ i, G i`.
Instead of `Σ i, G i`, we use the alias `Language.Structure.Sigma` which depends on `f`.
This way, Lean can infer what `L` and `f` are in the `Setoid` instance.
Otherwise we have a "cannot find synthesization order" error.
See also the discussion at
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/local.20instance.20cannot.20find.20synthesization.20order.20in.20porting
-/
@[nolint unusedArguments]
protected abbrev Sigma (f : ∀ i j, i ≤ j → G i ↪[L] G j) :=
Σ i, G i
