Theorems · Theorem · order theory

Sublocale.mem_mk

∀ {X : Type u_1} [inst : Order.Frame X] {a : X} (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier)
  (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier),
  a ∈ { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } ↔ a ∈ carrier

Defined in

Mathlib.Order.Sublocale

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

Order.Frame