Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox' (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)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
. intro h p hp; exact multiframe_def_multibox.mp h hp;
State after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
. intro h; apply multiframe_def_multibox.mpr; assumption;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro h p hp
State after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory
Tactic:
exact multiframe_def_multibox.mp h hp
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n] Ω₂

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n] Ω₂
Tactic:
apply multiframe_def_multibox.mpr
State after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
assumption
State after:
no goals