antitone

Mathlib.RingTheory.Filtration

URI: https://scilib.ai/kg/mathlib#Ideal.Filtration.antitone

English

The filtration N is antitone in its index: if i ≤ j then F.N(i) ⊇ F.N(j).

Русский

Фильтрация N антитонична по индексу: если i ≤ j тогда F.N(i) ⊇ F.N(j).

LaTeX

$$i \le j \Rightarrow F.N(i) \supseteq F.N(j)$$

Lean4

protected theorem antitone : Antitone F.N :=
  antitone_nat_of_succ_le F.mono

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

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

Разделы

Аффилиация

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