equiv_iff — Mathlib

English

Equivalence in the DirectLimit is determined by equality after projecting to a common higher index.

Русский

Эквивалентность в прямом пределе определяется равенством после отображения в общий более высокий индекс.

LaTeX

$$$x\\approx y \\iff (f_{x.fst,k}(x)=(f_{y.fst,k}(y)))$ for some k ≥ max(x.fst,y.fst)$$

Lean4

theorem equiv_iff {x y : Σˣ f} {i : ι} (hx : x.1 ≤ i) (hy : y.1 ≤ i) : x ≈ y ↔ (f x.1 i hx) x.2 = (f y.1 i hy) y.2 :=
  by
  cases x
  cases y
  refine ⟨fun xy => ?_, fun xy => ⟨i, hx, hy, xy⟩⟩
  obtain ⟨j, _, _, h⟩ := xy
  obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
  have h := congr_arg (f j k jk) h
  apply (f i k ik).injective
  rw [DirectedSystem.map_map, DirectedSystem.map_map] at *
  exact h

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