instance
small_transGen
{α : Type u_1}
(r : α → α → Prop)
[H : ∀ (x : α), Small.{u, u_1} { y : α // r x y }]
(x : α)
:
Small.{u, u_1} { y : α // Relation.TransGen r x y }
instance
small_transGen'
{α : Type u_1}
(r : α → α → Prop)
[∀ (x : α), Small.{u, u_1} { y : α // r y x }]
(x : α)
:
Small.{u, u_1} { y : α // Relation.TransGen r y x }
instance
small_reflTransGen
{α : Type u_1}
(r : α → α → Prop)
[H : ∀ (x : α), Small.{u, u_1} { y : α // r x y }]
(x : α)
:
Small.{u, u_1} { y : α // Relation.ReflTransGen r x y }
instance
small_reflTransGen'
{α : Type u_1}
(r : α → α → Prop)
[∀ (x : α), Small.{u, u_1} { y : α // r y x }]
(x : α)
:
Small.{u, u_1} { y : α // Relation.ReflTransGen r y x }