Theorems · Theorem · order theory

Function.frameMinimalAxioms

∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  Order.Frame.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
        (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) → Order.Frame.MinimalAxioms α

Pullback an Order.Frame.MinimalAxioms along an injection.

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

CompleteLatticeCompleteLattice