Totality of nominal lowering when every free variable is mapped.

def NFChoice.SemanticCore.PartialLowering.Mapped {n : ℕ} (rho : Var → Option (Fin n)) (support : Finset Var) : Prop

Proof-translation construction identified upstream as Mapped.

Equations

• NFChoice.SemanticCore.PartialLowering.Mapped rho support = ∀ x ∈ support, ∃ (i : Fin n), rho x = some i

theorem NFChoice.SemanticCore.PartialLowering.Mapped.mono {n : ℕ} {rho : Var → Option (Fin n)} {s t : Finset Var} (h : Mapped rho t) (hst : s ⊆ t) : Mapped rho s

theorem NFChoice.SemanticCore.PartialLowering.Mapped.lift {n : ℕ} {rho : Var → Option (Fin n)} {s : Finset Var} (h : Mapped rho s) : Mapped (liftRhoOption rho) s

theorem NFChoice.SemanticCore.PartialLowering.Mapped.update {n : ℕ} {rho : Var → Option (Fin n)} {s : Finset Var} (x : Var) (candidate : Fin n) (h : Mapped rho (s.erase x)) : Mapped (Function.update rho x (some candidate)) s

theorem NFChoice.SemanticCore.PartialLowering.lowerClassPredOption_exists {n : ℕ} (rho : Var → Option (Fin n)) (candidate : Fin n) (A : Class) (h : Mapped rho A.fv) : ∃ (f : Foundation.Formula n), lowerClassPredOption rho candidate A = some f

theorem NFChoice.SemanticCore.PartialLowering.lowerWffOption_exists {n : ℕ} (rho : Var → Option (Fin n)) (p : Wff) (h : Mapped rho p.fv) : ∃ (f : Foundation.Formula n), lowerWffOption rho p = some f

theorem NFChoice.SemanticCore.PartialLowering.lowerClosed_exists (p : Wff) (hp : p.fv = ∅) : ∃ (f : Foundation.Sentence), lowerClosed p = some f

theorem NFChoice.SemanticCore.PartialLowering.option_eq_some_getD {α : Type u_1} (o : Option α) (fallback : α) (h : ∃ (a : α), o = some a) : o = some (o.getD fallback)