wf
• r ∈ wf ⇔ (∀ s • (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s))
twf
| Parents |
| bin_rel |
| Constants |
|
wf
|
('a ↔ 'a) ℘ |
|
twf
|
('a ↔ 'a) ℘ |
| Definitions |
|
wf
|
⊢ ∀ r • r ∈ wf ⇔ (∀ s • (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s))
|
|
twf
|
⊢ ∀ r• r ∈ twf ⇔ r ∈ wf ∧ r ∈ Transitive |
| Theorems |
|
Dom_rest_thm
|
⊢ ∀ f s• Dom (s ⊲ f) = s ∩ Dom f |
|
rel_ext_Dom_thm
|
⊢ ∀ r s
• r = s ⇔ Dom r = Dom s ∧ (∀ x • x ∈ Dom r ∩ Dom s ⇒ (∀ y• (x, y) ∈ r ⇔ (x, y) ∈ s))
|
|
tran_tc_thm
|
⊢ ∀ r• r + ∈ Transitive |
|
tran_tc_thm2
|
⊢ ∀ r x y z • (x, y) ∈ r + ∧ (y, z) ∈ r + ⇒ (x, z) ∈ r +
|
|
⊆_tc_thm
|
⊢ ∀ r• r ⊆ r + |
|
∈_tc_thm
|
⊢ ∀ r x y• (x, y) ∈ r ⇒ (x, y) ∈ r + |
|
tc_decomp_thm
|
⊢ ∀ r x y
• (x, y) ∈ r + ∧ ¬ (x, y) ∈ r ⇒ (∃ z• (x, z) ∈ r + ∧ (z, y) ∈ r)
|
|
tcwf_lemma1
|
⊢ ∀ s r • r ∈ wf ⇒ (∀ x • (∀ y • (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s))
|
|
tcwf_lemma2
|
⊢ ∀ r • r ∈ wf ⇒ (∀ s • (∀ t• (∀ u• (u, t) ∈ r + ⇒ u ∈ s) ⇒ t ∈ s) ⇒ (∀ e• e ∈ s))
|
|
tc_wf_twf_thm
|
⊢ ∀ r• r ∈ wf ⇒ r + ∈ twf |
