pi_le_pi_iff

Mathlib.RingTheory.Ideal.Basic

URI: https://scilib.ai/kg/mathlib#Ideal.pi_le_pi_iff

← MathLib Explorer

English

For families of ideals I, J, pi I ≤ pi J if and only if I ≤ J.

Русский

Для семейств идей I, J верно: pi I ≤ pi J тогда и только если I ≤ J.

LaTeX

$$$\\operatorname{pi} I \\le \\operatorname{pi} J \\;\\Longleftrightarrow\\; I \\le J$$$

Lean4

@[simp]
theorem pi_le_pi_iff : pi I ≤ pi J ↔ I ≤ J
    where
  mp le i r hr := by classical simpa using le (single_mem_pi hr) i
  mpr le r hr i := le i (hr i)

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

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

Разделы

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

Аффилиация

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