biSup_comap_subtype_eq_top — Mathlib

English

Equality of iSup of comaps along subtype maps to top: iSup i iSup h p i equals top.

Русский

Равенство iSup комап вдоль подтипов равно топу: iSup i iSup h p i = топ.

LaTeX

$$$$ iSup (\\text{p(i)}) = \\top $$$$

Lean4

@[simp]
theorem biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤ :=
  by
  refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
  suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype
    by
    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
    exact hy
  suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
    simpa only [map_iSup, biSup_congr this]
  intro i hi
  rw [map_comap_eq, range_subtype, inf_eq_right]
  exact le_biSup p hi

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