mem_comap_jointlySurjectivePrecoverage_iff

English

If S covers X and X covers Y through f_i, then the composite family {f_i ∘ g_j} covers Y.

Русский

Если S покрывает X и X покрывает Y через f_i, то составные отображения {f_i ∘ g_j} покрывают Y.

LaTeX

$$comp_mem_coverings {ι} S X f hf σ Y g hg :=$$

Lean4

theorem mem_comap_jointlySurjectivePrecoverage_iff {X : C} {R : Presieve X} :
    R ∈ Types.jointlySurjectivePrecoverage.comap F X ↔
      ∀ x : F.obj X, ∃ (Y : C) (f : Y ⟶ X), R f ∧ x ∈ Set.range (F.map f) :=
  by
  rw [Precoverage.mem_comap_iff]
  refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨-, -, ⟨hf⟩, hi⟩ := h x
    exact ⟨_, _, hf, hi⟩
  · obtain ⟨Y, g, hg, hi⟩ := h x
    exact ⟨_, _, ⟨hg⟩, hi⟩

Похожие утверждения