exact Formula.Kripke.ValidOnFrame.morphism hSur hMorF (h hp)
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p✝ : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f
p : Formula α
hp : p ∈ T
⊢ F₂ ⊧ p
no goals