Transport of language families, witnesses, and width along equivalences

def GenLimit.FiniteWitness.transportClass {α : Type u_1} {β : Type u_2} (e : α ≃ β) (H : Set (Set α)) : Set (Set β)

Transport a language family along an equivalence of universes.

Equations

• GenLimit.FiniteWitness.transportClass e H = {K : Set β | ⇑e ⁻¹' K ∈ H}

noncomputable def GenLimit.FiniteWitness.transportAssignment {α : Type u_1} {β : Type u_2} (e : α ≃ β) (T : Set α → Finset α) (K : Set β) : Finset β

Transport finite witnesses along an equivalence of universes.

Equations

• GenLimit.FiniteWitness.transportAssignment e T K = Finset.map e.toEmbedding (T (⇑e ⁻¹' K))

@[simp]

theorem GenLimit.FiniteWitness.transportClass_inverse {α : Type u_1} {β : Type u_2} (e : α ≃ β) (H : Set (Set α)) : transportClass e.symm (transportClass e H) = H

theorem GenLimit.FiniteWitness.Valid.transport {α : Type u_1} {β : Type u_2} {H : Set (Set α)} {T : Set α → Finset α} (hT : Valid H T) (e : α ≃ β) : Valid (transportClass e H) (transportAssignment e T)

theorem GenLimit.FiniteWitness.HasBoundedWitnesses.transport {α : Type u_1} {β : Type u_2} {H : Set (Set α)} {d : ℕ} (h : HasBoundedWitnesses H d) (e : α ≃ β) : HasBoundedWitnesses (transportClass e H) d

theorem GenLimit.FiniteWitness.bounded_transport_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) (H : Set (Set α)) (d : ℕ) : HasBoundedWitnesses (transportClass e H) d ↔ HasBoundedWitnesses H d

theorem GenLimit.FiniteWitness.finiteWitnesses_transport {α : Type u_1} {β : Type u_2} {H : Set (Set α)} (h : HasFiniteWitnesses H) (e : α ≃ β) : HasFiniteWitnesses (transportClass e H)

theorem GenLimit.FiniteWitness.finiteWitnesses_transport_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) (H : Set (Set α)) : HasFiniteWitnesses (transportClass e H) ↔ HasFiniteWitnesses H

theorem GenLimit.FiniteWitness.width_le_of_witness_imp {α : Type u_1} {β : Type u_2} {F : Set (Set α)} {G : Set (Set β)} (hb : ∀ (d : ℕ), HasBoundedWitnesses G d → HasBoundedWitnesses F d) (hf : HasFiniteWitnesses G → HasFiniteWitnesses F) : separationWidth F ≤ separationWidth G

theorem GenLimit.FiniteWitness.width_eq_of_thresholds {α : Type u_1} {β : Type u_2} {H : Set (Set α)} {K : Set (Set β)} (hb : ∀ (d : ℕ), HasBoundedWitnesses H d ↔ HasBoundedWitnesses K d) (hf : HasFiniteWitnesses H ↔ HasFiniteWitnesses K) : separationWidth H = separationWidth K

theorem GenLimit.FiniteWitness.width_transport {α : Type u_1} {β : Type u_2} (e : α ≃ β) (H : Set (Set α)) : separationWidth (transportClass e H) = separationWidth H

theorem GenLimit.FiniteWitness.uus_transport {α : Type u_1} {β : Type u_2} {H : Set (Set α)} (hH : Generic.UUS H) (e : α ≃ β) : Generic.UUS (transportClass e H)