mem_sSup

Mathlib.LinearAlgebra.Span.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.mem_sSup

← MathLib Explorer

English

A variant of mem_sSup simplifying the right-hand side using standard membership lemmas.

Русский

Вариант mem_sSup с упрощением правой части с использованием стандартных лемм принадлежности.

LaTeX

$$∗$$

Lean4

theorem mem_sSup {s : Set (Submodule R M)} {m : M} : (m ∈ sSup s) ↔ ∀ N, (∀ p ∈ s, p ≤ N) → m ∈ N := by
  simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru