pigeonhole principle formally

[desert ether]

"we have 27 objects distributed in 26 buildings"
this is wrong, you're not putting 27 children in 26 buildings

each of them go in different ones

i thought of some alternative proofs but not a perfect application of pigeonhole yet, ofc the difficulty is to find the cages that make it work

you're not putting all 27 children in 26 buildings that, say, are in the range of one particular building

thre are other buildings of choice

if they're all consecutive the two farthest from each other will be seeing each other

problem is that this is not exactly "the worst case scenario", you have to argue that better

but even so

i think we can come up with some proof thinking in such ways but that will not be a conventional application of pigeonhole

[desert ether]

hmmm i thought of a solution

but i only apply pigeonhole after fixing one child in a building

would be more elegant if it was even before that

[desert ether]

tell me if you need another hint

Fix a child in a building to begin with.

Then there are 27 buildings where the other 26 children can't stay, they'd have to be distributed among the other 50

now there is a way to consider pairs of buildings out of those 50 that will work as your cages

[desert ether]

one the first was put in and the 26 in his vision range

27 buildings

1+26

[desert ether]

can you visualize where the 50 buildings left are situated?

maybe draw an imperfect sketch of the pokygon

can help

[desert ether]

no

remember that you want to solve with pigeonhole

you need to put more than n pigeons inn n cages for some n

what are the cages? remember the hints i gave

[desert ether]

26 children will go into 50 towers, one child per tower, correct?

let's say that you consider a partition of these towers into disjoint pairs of towers, say
{t1, t2}, {t3, t4}, ..., {t_{49}, t_{50}}

those are 25 pairs of (all distinct) towers

say that a child is "put in a pair P" if it is going inside a tower pertaining to the pair of towers P

so 26 children are being put in 25 pairs

by the pigeonhole principle, there will be a pair of towers where two children got put in

do you follow that?

that is the pigeonhole application

I just didn't tell you explicitly how exactly the pairing is and why it works

but the rest should be clear

[desert ether]

@finite hollow any progress?

[desert ether]

Yes! : }

that was the pairing i thought it, it's like quasi-symmetrical opposites

and I guess you understood the pigeonhole application too

yeah there are a lot of similar applications of pigeonhole

[formal whale]

a formal proof in lean, written by Kha.

import data.set.finite

-- we don't need no infinite sets here
open finset
open function

-- `fin n` is the type of the first `n` natural numbers
theorem pigeonhole (n m : ℕ) (f : fin n → fin m) : n > m → ¬(injective f) :=
assume : n > m,
-- proof of negation: show contradiction
assume : injective f,
show false,
-- using ‹n > m› (these quotes refer to proofs of known facts), we can prove the
-- contradiction by proving `n ≤ m`
from suffices n ≤ m,
  from nat.lt_le_antisymm ‹n > m› ‹n ≤ m›,
   -- the type `fin n` has `n` elements
calc n = fintype.card (fin n)         : by simp
   -- ... which we can also express as the cardinality of its universal set
   ... = card (univ : finset (fin n)) : rfl
   -- ... which is the same for its image under an injective function
   ... = card (image f univ)          : by simp [card_image_of_injective univ ‹injective f›]
   -- ... which is no larger than the universal set (in `fin m`)
   ... ≤ card (univ : finset (fin m)) : card_le_of_subset (subset_univ _)
   ... = fintype.card (fin m)         : rfl
   -- ... which has `m` elements
   ... = m                            : by simp