Elementary Penguin

@elempeng

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

233 Folgt492 Follower4.968 Posts

YouTube Bluesky

Ist das dein Profil?Übernimm es — dann gehört dir elempeng.dirty.social.Profil übernehmen

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!"$