Irreflexive Ne ∧ Symmetric Ne

Stream: Is there code for X?

[Snir Broshi]

For Eq there's docs#eq_equivalence, but for Ne I couldn't find proofs that it's irreflexive and symmetric.

[Ruben Van de Velde]

As theorems or instances of a particular class?

[Ruben Van de Velde]

@loogle Irreflexive

[loogle]

:search: Irreflexive, InvImage.irreflexive, and 11 more

[Ruben Van de Velde]

Yeah, nothing much there

[Snir Broshi]

For instances theres docs#IsIrrefl and docs#IsSymm, but those don't exist for docs#Ne either

[Snir Broshi]

If I add this, should I add the class version (IsIrrefl, IsSymm) or the prop version (Irreflexive, Symmetric)?
Eq has both IsEquiv and Equivalence, Iff has only IsEquiv, and Relation.EqvGen has only Equivalence.
Why do we need both versions of all these properties of relations?

[Snir Broshi]

Apparently there's also docs#Std.Irrefl and docs#Std.Symm, sigh

[Snir Broshi]

but I found docs#Ne.irrefl and docs#Ne.symm, which are close to what i asked

theorem foo1 {α : Type*} : Irreflexive (α := α) Ne := fun _ ↦ Ne.irrefl
theorem foo2 {α : Type*} : Symmetric (α := α) Ne := fun _ _ ↦ Ne.symm

[Ruben Van de Velde]

Yeah, I'm not sure what the status of these structures is