swapTrue_mem_C1 — Mathlib

English

If f is in the domain, then SwapTrue o f is in C1.

Русский

Если f принадлежит домену, то SwapTrue o f принадлежит C1.

LaTeX

$$∀ f, SwapTrue o f ∈ C1 C ho$$

Lean4

theorem swapTrue_mem_C1 (f : π (C1 C ho) (ord I · < o)) : SwapTrue o f.val ∈ C1 C ho :=
  by
  obtain ⟨f, g, hg, rfl⟩ := f
  convert hg
  dsimp +unfoldPartialApp [SwapTrue]
  ext i
  split_ifs with h
  · rw [ord_term ho] at h
    simpa only [← h] using hg.2.symm
  · simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]
    specialize hsC g hg.1 i
    intro h'
    contrapose! hsC
    exact ⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' h)⟩

Похожие утверждения