div_eq_filter_card — Mathlib

English

Let hb0: 0 < b and hc: a / b ≤ c. Then a / b equals the cardinality of { x ∈ Ico 1 c.succ | x*b ≤ a }.

Русский

Пусть hb0: 0 < b и hc: a / b ≤ c. Тогда a / b равняется мощности множества { x ∈ Ico 1 c.succ | x b ≤ a }.

LaTeX

$$$a / b = \#\{x ∈ Ico 1 c.succ \mid x \cdot b \le a\}$$$

Lean4

theorem div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) : a / b = #({x ∈ Ico 1 c.succ | x * b ≤ a}) :=
  calc
    a / b = #(Ico 1 (a / b).succ) := by simp
    _ = #({x ∈ Ico 1 c.succ | x * b ≤ a}) :=
      congr_arg _ <|
        Finset.ext fun x =>
          by
          have : x * b ≤ a → x ≤ c := fun h => le_trans (by rwa [le_div_iff_mul_le hb0]) hc
          simp [Nat.lt_succ_iff, le_div_iff_mul_le hb0]; tauto

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