English
For f,e, p, the equivalence between p.map e ∈ f.invtSubmodule and p ∈ (e.symm.conj f).invtSubmodule.
Русский
Эквивалентность между p.map e ∈ f.invtSubmodule и p ∈ (e.symm.conj f).invtSubmodule.
LaTeX
$$p.map e ∈ f.invtSubmodule \Longleftrightarrow p ∈ (e.symm.conj f).invtSubmodule$$
Lean4
/-- If `f(K) ≤ i(K)`, then `LinearMap.iterateMapComap` is not decreasing. -/
theorem iterateMapComap_le_succ (K : Submodule R N) (h : K.map f ≤ K.map i) (n : ℕ) :
f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K :=
by
nth_rw 2 [iterateMapComap]
rw [iterate_succ', Function.comp_apply, ← iterateMapComap, ← map_le_iff_le_comap]
induction n with
| zero => exact h
| succ n ih =>
simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]
calc
_ ≤ (f.iterateMapComap i n K).map i := map_comap_le _ _
_ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := by grw [← le_comap_map]
_ ≤ _ := by gcongr; exact ih
