galoisConnection_mul_div — Mathlib

English

A simp-styled corollary: BddAbove (Set.image e s) ↔ BddAbove s for an order isomorphism e.

Русский

Упрощённое следствие: BddAbove(Set.image e s) ⇔ BddAbove s для порядкового изоморфизма e.

LaTeX

$$$$ BddAbove( Set.image e s ) \\;\\Longleftrightarrow\\; BddAbove(s). $$$$

Lean4

theorem galoisConnection_mul_div {k : ℕ} (h : 0 < k) : GaloisConnection (fun n => n * k) fun n => n / k := fun _ _ =>
  (le_div_iff_mul_le h).symm

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