mem_map_objs_iff — Mathlib

English

An object d lies in the objects of map φ hφ S iff there exists c ∈ S.objs with φ.obj c = d.

Русский

Объект d принадлежит множеству объектов map φ hφ S тогда и только тогда, когда существует c ∈ S.objs с φ.obj c = d.

LaTeX

$$$d \in (map φ hφ S).objs \iff \exists c \in S.objs, φ.obj c = d$$$

Lean4

theorem mem_map_objs_iff (hφ : Function.Injective φ.obj) (d : D) : d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d :=
  by
  dsimp [objs, map]
  constructor
  · rintro ⟨f, hf⟩
    change Map.Arrows φ hφ S d d f at hf; rw [Map.arrows_iff] at hf
    obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf
    exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩
  · rintro ⟨c, ⟨γ, γS⟩, rfl⟩
    exact ⟨φ.map γ, ⟨γ, γS⟩⟩

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