Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.frame_def_box (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (CanonicalFrame L).Rel Ω₁ Ω₂ ↔ ∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
rfl
State after:
no goals