iInf_invariant — Mathlib

English

If each i-indexed submodule p(i) is f-invariant (f(v) ∈ p(i) for all v ∈ p(i)), then the infimum iInf p is f-invariant as well.

Русский

Если все p(i) инвариантны относительно f, то и их инфимума по i инвариантно относительно f.

LaTeX

$$$\forall i,\ \forall v\, (v \in p(i) \Rightarrow f v \in p(i)) \Rightarrow \forall v\ (v \in iInf p \Rightarrow f v \in iInf p)$$$

Lean4

/-- The infimum of a family of invariant submodule of an endomorphism is also an invariant
submodule. -/
theorem _root_.LinearMap.iInf_invariant {σ : R →+* R} {ι : Sort*} (f : M →ₛₗ[σ] M) {p : ι → Submodule R M}
    (hf : ∀ i, ∀ v ∈ p i, f v ∈ p i) : ∀ v ∈ iInf p, f v ∈ iInf p :=
  by
  simp only [mem_iInf]
  exact fun v a i ↦ hf i v (a i)

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