English
If the ambient set X is finite and a block B satisfies |X| < 2|B|, then B is the whole X.
Русский
Если множество Xнема конечное и блок B удовлетворяет неравенству |X| < 2|B|, то B равно всему X.
LaTeX
$$$|X| < 2\,|B| \;\Rightarrow\; B = \mathrm{univ}$$$
Lean4
/-- A too large block is equal to `univ` -/
@[to_additive /-- A too large block is equal to `univ` -/
]
theorem eq_univ_of_card_lt [hX : Finite X] (hB : IsBlock G B) (hB' : Nat.card X < Set.ncard B * 2) : B = Set.univ :=
by
rcases Set.eq_empty_or_nonempty B with rfl | hB_ne
· simp only [Set.ncard_empty, zero_mul, not_lt_zero'] at hB'
have key := hB.ncard_block_mul_ncard_orbit_eq hB_ne
rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] at hB'
interval_cases (orbit G B).ncard
· rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key
exact (IsEmpty.exists_iff.mp hB_ne).elim
· rw [mul_one, ← Set.ncard_univ] at key
rw [Set.eq_of_subset_of_ncard_le (Set.subset_univ B) key.ge]
