Theorem: ConverseWellFounded.iff_has_max (Logic/Vorspiel/BinaryRelations.lean)

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
r : α → α → Prop
⊢ ConverseWellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r m x
Tactic:
simp [ConverseWellFounded, WellFounded.wellFounded_iff_has_min, flip]
State after:
no goals