Theorems · Theorem · number theory

Northcott.comp_of_bddAbove

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) (h' : β → γ) [inst : Preorder β] [inst_1 : LE γ]
  [Northcott h], (∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})) → Northcott (h' ∘ h)

A composition h' ∘ h is Northcott when h is Northcott and preimages of bounded above sets under h' are bounded above.

Defined in

Mathlib.Order.Northcott

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderLENorthcott