English
Let cond be an LEComap for continuous map f, and h a comparison between discrete quotients B ≤ B'. Then the map respects ofLE and map f as described: ofLE h (map f cond a) = map f (cond.mono le_rfl h) a.
Русский
Пусть cond — LEComap для непрерывной карты f, и h отношение между дискретными факторными множествами B ≤ B'. Тогда отображение сохраняет ofLE и map f по описанию: ofLE h (map f cond a) = map f (cond.mono le_rfl h) a.
LaTeX
$$$ \text{ofLE } h (\text{map } f \; cond\; a) = \text{map } f (cond.mono\; le\_rfl\; h)\; a $$$
Lean4
@[simp]
theorem ofLE_map (cond : LEComap f A B) (h : B ≤ B') (a : A) : ofLE h (map f cond a) = map f (cond.mono le_rfl h) a :=
by
rcases a with ⟨⟩
rfl
