mem_degreeLT — Mathlib

English

For any R, n, and f ∈ R[X], f ∈ degreeLT(R,n) if and only if deg f < n.

Русский

Для любого R, натурального n и f ∈ R[X], f ∈ degreeLT(R,n) тогда и только тогда, когда deg f < n.

LaTeX

$$$f \in \operatorname{degreeLT}_R(n) \iff \deg f < n.$$$

Lean4

theorem mem_degreeLT {n : ℕ} {f : R[X]} : f ∈ degreeLT R n ↔ degree f < n :=
  by
  rw [degreeLT, Submodule.mem_iInf]
  conv_lhs => intro i; rw [Submodule.mem_iInf]
  rw [degree, Finset.max_eq_sup_coe]
  rw [Finset.sup_lt_iff ?_]
  rotate_left
  · apply WithBot.bot_lt_coe
  conv_rhs =>
    simp only [mem_support_iff]
    intro b
    rw [Nat.cast_withBot, WithBot.coe_lt_coe, lt_iff_not_ge, Ne, not_imp_not]
  rfl

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