r_of_le — Mathlib

English

A compatibility condition for two-stage maps in a directed system: composing maps equals the map to the composed index.

Русский

Совместимость двухступенчатых отображений в направленной системе: композиция тождественно равна отображению по составному индексу.

LaTeX

$$$f j k hjk (f i j hij x) = f i k (hij.trans hjk) x$ in a directed system.$$

Lean4

theorem r_of_le (x : Σ i, F i) (i : ι) (h : x.1 ≤ i) : (setoid f).r x ⟨i, f _ _ h x.2⟩ :=
  ⟨i, h, le_rfl, (map_map' _ _ _ _).symm⟩

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