Brendan Zabarauskas on Twitter: "@dan_abramov These very much remind me of how you do proofs in an theorem prover, like Lean, Coq, or Isabelle! Also reminded of “Structured derivations: a unified proof style for teaching mathematics” by Ralph-Johan Back: https://t.co/lUXwEXwpWh" / Twitter

yasss i wasn’t sure i’ll get somewhere with this but looks like it unfolded nicely

$Show that it's a set of all partial functions from X to Y - S = U U { ({ Y'^X' for Y' in 2^Y }) for X' in 2^X' } - Show that f ∈ S => f a partial function from X to Y - Suppose f ∈ S - Show f is partial function from X to Y - Show f is a function from some X' ∈ X to some Y' ∈ Y - Let A = U { ({ Y'^X' for Y' in 2^Y }) for X' in 2^X' } - f ∈ U A <=> f ∈ B for some B ∈ A - Take that B ∈ A - So, B ∈ U { ({ Y'^X' for Y' in 2^Y }) for X' in 2^X' } - Let C = { ({ Y'^X' for Y' in 2^Y }) for X' in 2^X' } - B ∈ U C <=> B ∈ D for some D ∈ C - Take that D ∈ C - So, D is { Y'^X' for Y' in 2^Y } for some X' in 2^X - Take that X' in 2^X' - B ∈ D, so B is Y'^X' for some Y' in 2^Y - That that Y' in 2^Y - f ∈ B, so f ∈ Y'^X' - So, f is a function from X' to Y'.$

read image description

ALT

Conversation