Theorem IsConcreteLE.exists_of_lt

Modification history

2026-09-15 16:52
Mathlib/Data/SetLike/Basic.lean
refactor(Data/SetLike): generalise `IsConcreteLE` (#42666) …
Added IsConcreteLE.exists_of_ltView on Github →