krullDim_le_of_strictComono_and_surj

English

If f is strictly monotone and surjective, then krullDim β ≤ krullDim α.

Русский

Если f строго монотонна и сюръективна, тогда krullDim β ≤ krullDim α.

LaTeX

$$\operatorname{krullDim}(\beta) \le \operatorname{krullDim}(\alpha) \\text{(surjective, strictly monotone } f)$$

Lean4

theorem krullDim_le_of_strictComono_and_surj (f : α → β) (hf : ∀ ⦃a b⦄, f a < f b → a < b)
    (hf' : Function.Surjective f) : krullDim β ≤ krullDim α :=
  iSup_le fun p ↦ le_sSup ⟨p.comap _ hf hf', rfl⟩

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