22 lines
557 B
Plaintext
22 lines
557 B
Plaintext
import Mathlib.Data.Set.Basic
|
||
import Mathlib.SetTheory.ZFC.Basic
|
||
|
||
import Common.Set.OrderedPair
|
||
|
||
/-! # Enderton.Chapter_3
|
||
|
||
Relations and Functions
|
||
-/
|
||
|
||
namespace Enderton.Set.Chapter_3
|
||
|
||
/--
|
||
If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
|
||
-/
|
||
theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
|
||
: Set.OrderedPair x y ∈ 𝒫 𝒫 C := by
|
||
have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
|
||
have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
|
||
exact Set.mem_mem_imp_pair_subset hxs hxys
|
||
|
||
end Enderton.Set.Chapter_3 |