biSup_comap_eq_top_of_surjective — Mathlib

English

If p ≤ p' and p ⊔ ker f < p' ⊔ ker f, then map f p < map f p'.

Русский

Если p ⊆ p' и p ⊔ ker f < p' ⊔ ker f, тогда map f p < map f p'.

LaTeX

$$$p \le p' \land p \;⊔\; \ker f < p' \;⊔\; \ker f \Rightarrow \operatorname{map}_f p < \operatorname{map}_f p'$$$

Lean4

theorem biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempty) (p : ι → Submodule R₂ M₂)
    (hp : ⨆ i ∈ s, p i = ⊤) (f : M →ₛₗ[τ₁₂] M₂) (hf : Surjective f) : ⨆ i ∈ s, (p i).comap f = ⊤ :=
  by
  obtain ⟨k, hk⟩ := hs
  suffices (⨆ i ∈ s, (p i).comap f) ⊔ LinearMap.ker f = ⊤ by rw [← this, left_eq_sup];
    exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)
  rw [iSup_subtype'] at hp ⊢
  rw [← comap_map_eq, map_iSup_comap_of_surjective hf, hp, comap_top]

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