English
Given a filter f with realizer F and a family of filters m i with realizers G i, there is a realizer for the bind f.bind m, whose underlying index is a Sigma-type and whose value aggregates the realizations of the G i over the indices in F.
Русский
Пусть есть фильтр f с реализатором F и семейство фильтров m_i с реализаторами G_i; существует реализатор для связки f.bind m, базирующийся на сигма-типе и объединяющий реализации G_i над индексами из F.
LaTeX
$$$\\text{Realizer}(f \\text{.bind } m) = \\langle \\Sigma s : F.\\sigma, \\; \\text{f-map} , \\; \\text{inf and mem-conditions} \\rangle$ (конструкция включает объединение по i в F.F s).$$
Lean4
/-- Construct a realizer for filter bind -/
protected def bind {f : Filter α} {m : α → Filter β} (F : f.Realizer) (G : ∀ i, (m i).Realizer) : (f.bind m).Realizer :=
⟨Σ s : F.σ, ∀ i ∈ F.F s, (G i).σ,
{ f := fun ⟨s, f⟩ ↦ ⋃ i ∈ F.F s, (G i).F (f i (by assumption))
pt := ⟨F.F.pt, fun i _ ↦ (G i).F.pt⟩
inf := fun ⟨a, f⟩ ⟨b, f'⟩ ↦
⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f i (F.F.inf_le_left _ _ h)) (f' i (F.F.inf_le_right _ _ h))⟩
inf_le_left := fun _ _ _ ↦ by
simp only [mem_iUnion, forall_exists_index]
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_left _ _ h₁, (G i).F.inf_le_left _ _ h₂⟩
inf_le_right := fun _ _ _ ↦ by
simp only [mem_iUnion, forall_exists_index]
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_right _ _ h₁, (G i).F.inf_le_right _ _ h₂⟩ },
filter_eq <|
Set.ext fun _ ↦ by
obtain ⟨_, F, _⟩ := F; subst f
simp only [CFilter.toFilter, iUnion_subset_iff, Sigma.exists, Filter.mem_sets, mem_bind]
exact
⟨fun ⟨s, f, h⟩ ↦ ⟨F s, ⟨s, Subset.refl _⟩, fun i H ↦ (G i).mem_sets.2 ⟨f i H, fun _ h' ↦ h i H h'⟩⟩,
fun ⟨_, ⟨s, h⟩, f⟩ ↦
let ⟨f', h'⟩ := Classical.axiom_of_choice fun i : F s ↦ (G i).mem_sets.1 (f i (h i.2))
⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩⟩
