TwoPointing.fst_ne_snd

theorem TwoPointing.fst_ne_snd : ∀ {α : Type u_3} (self : TwoPointing α), self.toProd.1 ≠ self.toProd.2

This theorem states that for any two-pointed set, represented as `TwoPointing α` where `α` is a type, the first element and the second element (obtained using `fst` and `snd` respectively) of the tuple representation of the set are always distinct. That means, no matter what the type `α` is, if we have a two-pointed set of that type, the two points of the set can never be the same.

More concisely: For any two-pointed set `TwoPointing α`, the first and second elements of the underlying tuple are distinct.