def Rel.reflTransGen₁ {α : Type u} (r : Rel α α) (s : Set α) : Set α

Equations

• r.reflTransGen₁ s = ⋃ x ∈ s, {y : α | r y x}

theorem Rel.card_reflTransGen₁_lt {α : Type u} {r : Rel α α} {κ : Cardinal.{u}} (hr : ∀ (y : α), Cardinal.mk ↑{x : α | r x y} < κ) (hκ : κ.IsRegular) (s : Set α) (hs : Cardinal.mk ↑s < κ) : Cardinal.mk ↑(r.reflTransGen₁ s) < κ

def Rel.reflTransGenₙ {α : Type u} (r : Rel α α) : ℕ → Set α → Set α

Equations

• r.reflTransGenₙ = Nat.iterate r.reflTransGen₁

theorem Rel.card_reflTransGenₙ_lt {α : Type u} {r : Rel α α} {κ : Cardinal.{u}} (hr : ∀ (y : α), Cardinal.mk ↑{x : α | r x y} < κ) (hκ : κ.IsRegular) (s : Set α) (hs : Cardinal.mk ↑s < κ) (n : ℕ) : Cardinal.mk ↑(r.reflTransGenₙ n s) < κ

def Rel.reflTransGen' {α : Type u} (r : Rel α α) : Rel α α

Equations

• r.reflTransGen' x y = (x ∈ ⋃ (n : ℕ), {x : α | r.reflTransGenₙ n {y} x})

theorem Rel.reflTransGen'_iff {α : Type u} (r : Rel α α) (x y : α) : r.reflTransGen' x y ↔ Relation.ReflTransGen r x y

theorem Rel.card_reflTransGen_lt {α : Type u} {r : Rel α α} {κ : Cardinal.{u}} (hr : ∀ (y : α), Cardinal.mk ↑{x : α | r x y} < κ) (hκ₁ : κ.IsRegular) (hκ₂ : Cardinal.aleph0 < κ) (y : α) : Cardinal.mk ↑{x : α | Relation.ReflTransGen r x y} < κ

theorem Rel.card_transGen_lt {α : Type u} {r : Rel α α} {κ : Cardinal.{u}} (hr : ∀ (y : α), Cardinal.mk ↑{x : α | r x y} < κ) (hκ₁ : κ.IsRegular) (hκ₂ : Cardinal.aleph0 < κ) (y : α) : Cardinal.mk ↑{x : α | Relation.TransGen r x y} < κ

theorem Rel.card_reflTransGen_le {α : Type u} {r : Rel α α} {κ : Cardinal.{u}} (hr : ∀ (y : α), Cardinal.mk ↑{x : α | r x y} ≤ κ) (hκ : Cardinal.aleph0 ≤ κ) (y : α) : Cardinal.mk ↑{x : α | Relation.ReflTransGen r x y} ≤ κ

theorem Rel.card_transGen_le {α : Type u} {r : Rel α α} {κ : Cardinal.{u}} (hr : ∀ (y : α), Cardinal.mk ↑{x : α | r x y} ≤ κ) (hκ : Cardinal.aleph0 ≤ κ) (y : α) : Cardinal.mk ↑{x : α | Relation.TransGen r x y} ≤ κ