English
Let f be a continuous map and cond be a LEComap relating A to B; for any h with B ≤ B', the two ways of refining the quotient commute: composing with ofLE h after map f cond is the same as mapping f with the adjusted condition cond.mono le_rfl h.
Русский
Пусть f — непрерывное отображение и cond — LEComap между A и B; для любого h с условием B ≤ B', два способа повышения уточнения частично совпадают: композиция ofLE h после map f cond равна map f (cond.mono le_rfl h).
LaTeX
$$$ (\\mathrm{ofLE}\\, h) \\circ (\\mathrm{map}\\ f\\ cond) = \\mathrm{map}\\ f\\bigl(\\mathrm{cond.mono}\\ \\mathrm{le\\_rfl}\\ h \\bigr) $$$
Lean4
@[simp]
theorem ofLE_comp_map (cond : LEComap f A B) (h : B ≤ B') : ofLE h ∘ map f cond = map f (cond.mono le_rfl h) :=
funext <| ofLE_map cond h
