sup — Mathlib

English

If I and J are fractional submodules, then their supremum I ⊔ J is fractional.

Русский

Если I и J -- дробные подмодули, то их наибольшая верхняя граница I ⊔ J тоже дробная.

LaTeX

$$IsFractional S I ∧ IsFractional S J ⇒ IsFractional S (I ⊔ J)$$

Lean4

theorem _root_.IsFractional.sup {I J : Submodule R P} : IsFractional S I → IsFractional S J → IsFractional S (I ⊔ J)
  | ⟨aI, haI, hI⟩, ⟨aJ, haJ, hJ⟩ =>
    ⟨aI * aJ, S.mul_mem haI haJ, fun b hb =>
      by
      rcases mem_sup.mp hb with ⟨bI, hbI, bJ, hbJ, rfl⟩
      rw [smul_add]
      apply isInteger_add
      · rw [mul_smul, smul_comm]
        exact isInteger_smul (hI bI hbI)
      · rw [mul_smul]
        exact isInteger_smul (hJ bJ hbJ)⟩

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