lean_workbook_plus_62355

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

let's take $X=$ { $A_i$ satisfying the conditions} and $Y=$ { $A_i^C$ such that $A_i\in X$ }\nNOTE: $A_i^C=S$ \ $A_i$ is the complement of $A_i$ in $S$ \n\nobviously $\left |X\bigcap Y \right |= 0$ and $|X|=|Y|=m$ \n\nso $2m=|X|+|Y|< 2^n:$ the number of elements of $S$ \nthen $m\le 2^{n-1}-1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62355  (m n : ℕ)
  (h₀ : 0 < m ∧ 0 < n)
  (h₁ : 2 * m < 2^n) :
  m ≤ 2^(n - 1) - 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph