inf_right — Mathlib

English

If I is fractional, then I ∩ J is fractional for every submodule J.

Русский

Если I дробный, то I ∩ J дробный для каждого подмодуля J.

LaTeX

$$IsFractional S I → ∀ J, IsFractional S (I ⊓ J)$$

Lean4

theorem _root_.IsFractional.inf_right {I : Submodule R P} : IsFractional S I → ∀ J, IsFractional S (I ⊓ J)
  | ⟨aI, haI, hI⟩, J =>
    ⟨aI, haI, fun b hb => by
      rcases mem_inf.mp hb with ⟨hbI, _⟩
      exact hI b hbI⟩

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