Zulip Chat Archive
Stream: new members
Topic: Using an axiom with ∃!
Quinn Culver (Nov 12 2022 at 04:15):
Can I use ∃! like this?
axiom two_points_unique_line (p₁ p₂ : Point)(h : p₁ ≠ p₂) : ∃! l : Line, (lies_on p₁ l) ∧ (lies_on p₂ l)
IF so, once I have gl: lies_on p₁ l ∧ lies_on p₂ l and gl₀: lies_on p₁ l₀ ∧ lies_on p₂ l₀ in my local context, how can I use two_points_unique_line to show l=l_0?
Junyan Xu (Nov 12 2022 at 04:37):
Last updated: Dec 20 2023 at 11:08 UTC