Bryan Gin-ge Chen bryangingechen

here to learn

38 followers · 82 following

@blockspins

View GitHub Profile

bryangingechen / .block

Created July 20, 2020 15:13

leanBrowser.js demo

license: mit

bryangingechen / .block

Last active February 13, 2019 18:09

circle pack example

license: mit

bryangingechen / .block

Last active May 20, 2021 10:43

circle pack with file input

license: mit

bryangingechen / card_subsets_binomial.lean

Created November 13, 2018 18:03

	import data.nat.choose

	open finset nat

	lemma not_mem_subset_range {n : ℕ} {t : finset ℕ} (H : t ⊆ range n) : n ∉ t :=
	λ h, not_mem_range_self (mem_of_subset H h)

	lemma card_subsets_of_range_eq_choose (n k : ℕ) :
	card ((powerset (range n)).filter (λ t, card t = k)) = choose n k :=
	match n, k with

bryangingechen / .block

Last active July 12, 2018 07:03

Square lattice spring network

	license: gpl-3.0
	height: 960