English
Let cond be a LEComap f A B, let h: A' ≤ A, and c ∈ A'. Then map f cond (ofLE h c) = map f (cond.mono h le_rfl) c; this expresses how map f cond commutes with refining the domain quotient.
Русский
Пусть cond — LEComap f A B, h: A' ≤ A и c ∈ A'. Тогда map f cond (ofLE h c) = map f (cond.mono h le_rfl) c; это выражает, что map f cond сохраняет совместимость при уточнении проекции.
LaTeX
$$$\\mathrm{map}\\ f\\ cond\\bigl(\\mathrm{ofLE}\\ h\\ c\\bigr) = \\mathrm{map}\\ f\\bigl(\\mathrm{cond.mono}\\ h\\ \\mathrm{le\\_rfl}\\bigr)\\ c$$$
Lean4
@[simp]
theorem map_ofLE (cond : LEComap f A B) (h : A' ≤ A) (c : A') : map f cond (ofLE h c) = map f (cond.mono h le_rfl) c :=
by
rcases c with ⟨⟩
rfl
