mem_of_mem_of_le

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.mem_of_mem_of_le

English

If x ∈ I and I ≤ J then x ∈ J.

Русский

Если x ∈ I и I ≤ J, то x ∈ J.

LaTeX

$$$ x \\in I \\Rightarrow I \\le J \\Rightarrow x \\in J $$$

Lean4

@[trans]
theorem mem_of_mem_of_le {x : P} {I J : Ideal P} : x ∈ I → I ≤ J → x ∈ J :=
  @Set.mem_of_mem_of_subset P x I J

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

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

Разделы

Аффилиация

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