map_comp_ofLE — Mathlib

English

For cond and h with h : A' ≤ A, the composition map f cond composed with ofLE h equals the map f applied to cond with the refined argument: map f cond ∘ ofLE h = map f (cond.mono h le_rfl).

Русский

Для cond и h с h : A' ≤ A имеет место равенство: map f cond ∘ ofLE h = map f (cond.mono h le_rfl).

LaTeX

$$$\\mathrm{map}\\ f\\ cond\\circ \\mathrm{ofLE}\\ h = \\mathrm{map}\\ f\\bigl(\\mathrm{cond.mono}\\ h\\ \\mathrm{le\\_rfl}\\bigr)$$$

Lean4

@[simp]
theorem map_comp_ofLE (cond : LEComap f A B) (h : A' ≤ A) : map f cond ∘ ofLE h = map f (cond.mono h le_rfl) :=
  funext <| map_ofLE cond h

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