English
See 157707 (fst projection) for projection of directedness to first component.
Русский
См. пункт 157707: направленность проекции на первую компоненту.
LaTeX
$$$\text{DirectedOn fst} \Rightarrow \text{DirectedOn } (\text{fst}'' d).$$$
Lean4
/-- The setoid on the sigma type defining the direct limit. -/
def setoid : Setoid (Σ i, F i)
where
r x y := ∃ᵉ (i) (hx : x.1 ≤ i) (hy : y.1 ≤ i), f _ _ hx x.2 = f _ _ hy y.2
iseqv :=
⟨fun x ↦ ⟨x.1, le_rfl, le_rfl, rfl⟩, fun ⟨i, hx, hy, eq⟩ ↦ ⟨i, hy, hx, eq.symm⟩,
fun ⟨j, hx, _, jeq⟩ ⟨k, _, hz, keq⟩ ↦
have ⟨i, hji, hki⟩ := exists_ge_ge j k
⟨i, hx.trans hji, hz.trans hki, by rw [← map_map' _ hx hji, ← map_map' _ hz hki, jeq, ← keq, map_map', map_map']⟩⟩
