Elementary Penguin

@elempeng

Elementary Penguin is an okapi at the San Diego Zoo. He likes math and hates food.

233 Following492 Followers4,968 Posts

YouTube Bluesky

Is this your profile?Claim it and elempeng.dirty.social is yours.Claim profile

Elementary Penguin@elempeng· 17d

Red tailed hawk

Elementary Penguin@elempeng· 18d

An old-fashioned amusement park sign that reads “ride the thunderbolt” it appears to be a cloud with a lightning bolt through it

Elementary Penguin@elempeng· 19d

doing this for leisure because ???

$a Lean 4 proof that if f is a coordinate function for the line A B such that f(A) = 0 and f(B) > 0, then the ray AB = {P on line A B : f(P) >= 0}. there is a blue checkmark next to the following code: theorem ray_from_cf (A B : Point) (hAB : A ≠ B) (l : Line) (hAl : A ∈ l) (hBl : B ∈ l) (cf : CoordFn l) (hfA_zero : cf.fn A = 0) (hfB_pos : cf.fn B > 0) : Ray A B = {P | P ∈ l ∧ cf.fn P ≥ 0} := by ext X simp constructor · intro h have hXl := on_line_of_on_ray l hAl hBl h refine ⟨hXl, ?_⟩ rcases h with ha | ha · rcases ha with hb | hb · rcases hb with hc | hc all_goals subst hc; linarith · have ⟨hleft, hright⟩ := btwn_points_mp l A B X hAl hBl hXl cf (hfA_zero ▸ hfB_pos) hb linarith · obtain ⟨hAB, hAX, hBX, hdist, hcol⟩ := ha rcases lt_or_gt_of_ne (mt (cf.injOn A X hAl hXl) hAX) with hb | hb · linarith · exfalso rw [d_symm A B, d_symm B X, d_symm A X, add_comm] at hdist have ⟨hleft, hright⟩ := btwn_points_mp l X A B hXl hAl hBl cf hb ⟨hBX.symm, hAX.symm, hAB.symm, hdist, collinear_symm hcol⟩ linarith · intro ⟨hXl, hfX_nonneg ⟩ rw [le_iff_lt_or_eq] at hfX_nonneg unfold Ray unfold Sgmt simp rcases hfX_nonneg with h | h · rw [hfA_zero.symm] at h have hAX := mt (congrArg cf.fn) (ne_of_lt h) rcases lt_trichotomy (cf.fn X) (cf.fn B) with ha | ha | ha · have hBX := Ne.symm (mt (congrArg cf.fn) (ne_of_lt ha)) have hAXB := btwn_points_mpr l A X B hAX hBX hAl hXl hBl cf h ha; tauto · have hXB := cf.injOn B X hBl hXl ha.symm; tauto · have hBX := Ne.symm (mt (congrArg cf.fn) (ne_of_lt ha)) have hABX := btwn_points_mpr l A B X hAB hBX hAl hBl hXl cf (hfA_zero ▸ hfB_pos) ha; tauto · have hXA := cf.injOn A X hAl hXl (hfA_zero ▸ h); tauto a message on the right says "Goals accomplished!"$