Placements.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PartitionConsistency.SmallPlacements.extend_embedding line 13
Source documentation
A partial injection on a subset of a smaller set can be completed to an injection into the larger infinite set. This is a ground-choice construction.
```
theorem extend_embedding [Infinite β] (h : #α < #β) {s : Set α} (f : s ↪ β) :
    ∃ g : α ↪ β, ∀ x : s, g x = f x := by
…
```
theorem OAI.PartitionConsistency.SmallPlacements.embedding_cover line 39
Source documentation
An embedding into a larger infinite set can be chosen to cover a prescribed subset whose cardinality does not exceed that of its domain.
```
theorem embedding_cover [Infinite β] (h : #α < #β) {s : Set β} (hs : #s ≤ #α) :
    ∃ g : α ↪ β, s ⊆ Set.range g := by
…
```
theorem OAI.PartitionConsistency.SmallPlacements.extend_embedding_cover line 53
Source documentation
Complete an existing partial injection and cover a prescribed small subset at the same time. No value already prescribed is altered.
```
theorem extend_embedding_cover [Infinite β] (h : #α < #β) {s : Set α}
    (f : s ↪ β) {J : Set β} (hJ : #J ≤ #(sᶜ : Set α)) :
    ∃ g : α ↪ β, (∀ x : s, g x = f x) ∧ J ⊆ Set.range g := by
…
```
theorem OAI.PartitionConsistency.SmallPlacements.extend_permutation line 100
Source documentation
A small ground partial placement extends to a permutation.
```
theorem extend_permutation {s : Set α} (f : s ↪ α) (hs : #s < #α) :
    ∃ π : Equiv.Perm α, ∀ x : s, π x = f x :=
…
```
theorem OAI.PartitionConsistency.SmallPlacements.move_off line 106
Source documentation
Move a small set off any other small set, leaving a specified common root fixed. The complement of the forbidden union supplies the fresh labels.
```
theorem move_off [Infinite α] {s t r : Set α}
    (hst : #(s ∪ t ∪ r : Set α) < #α) :
    ∃ π : Equiv.Perm α, (∀ x ∈ r, π x = x) ∧
      Disjoint (π '' (s \ r)) (t ∪ r) := by
…
```