English
For a family of filters f i with realizers F i, there is a realizer for the indexed supremum ⨆ i, f i, constructed via a dependent-join with anEquiv between a Sigma-type and a product of realizers.
Русский
Для семейства фильтров f_i с реализаторами F_i существует реализатор для индексированного объединения ⨆ i, f_i, получаемый через зависимую связку и эквиваленцию между сигма-типом и произведением реализаторов.
LaTeX
$$$\\text{Realizer}(\\bigsqcup_i f_i) = \\text{Realizer.iSup}(F)$, with a formal equivalence $\\Sigma _{i} (F i)$ ≃ (∀ i, F i.σ)$.$$
Lean4
/-- Construct a realizer for indexed supremum -/
protected def iSup {f : α → Filter β} (F : ∀ i, (f i).Realizer) : (⨆ i, f i).Realizer :=
let F' : (⨆ i, f i).Realizer :=
(Realizer.bind Realizer.top F).ofEq <| filter_eq <| Set.ext <| by simp [Filter.bind, iSup_sets_eq]
F'.ofEquiv <|
show (Σ _ : Unit, ∀ i : α, True → (F i).σ) ≃ ∀ i, (F i).σ from
⟨fun ⟨_, f⟩ i ↦ f i ⟨⟩, fun f ↦ ⟨(), fun i _ ↦ f i⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩
