mem_inf

Mathlib.RingTheory.Ideal.Lattice

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

English

For ideals I and J, x ∈ I ∩ J if and only if x ∈ I and x ∈ J.

Русский

Для идеалов I и J верно: x ∈ I ∩ J тогда и только тогда, когда x ∈ I и x ∈ J.

LaTeX

$$$x \\in I \\cap J \\iff x \\in I \\land x \\in J$$$

Lean4

theorem mem_inf {I J : Ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J :=
  Iff.rfl

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

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

Разделы

Аффилиация

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