Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2020 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson
! This file was ported from Lean 3 source module order.atoms.finite
! leanprover-community/mathlib commit d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Finite
import Mathlib.Order.Atoms
/-!
# Atoms, Coatoms, Simple Lattices, and Finiteness
This module contains some results on atoms and simple lattices in the finite context.
## Main results
* `Finite.to_isAtomic`, `Finite.to_isCoatomic`: Finite partial orders with bottom resp. top
are atomic resp. coatomic.
-/
variable { α β : Type _ }
namespace IsSimpleOrder
section DecidableEq
/- It is important that `IsSimpleOrder` is the last type-class argument of this instance,
so that type-class inference fails quickly if it doesn't apply. -/
instance ( priority := 200) { α } [ DecidableEq : Sort ?u.17 → Sort (max1?u.17) α ] [ LE α ] [ BoundedOrder : (α : Type ?u.29) → [inst : LE α Type ?u.29 α ] [ IsSimpleOrder α ] :
Fintype α :=
Fintype.ofEquiv Bool equivBool . symm : {α : Sort ?u.199} → {β : Sort ?u.198} → α ≃ β β ≃ α
end DecidableEq
end IsSimpleOrder
namespace Fintype
namespace IsSimpleOrder
variable [ PartialOrder α ] [ BoundedOrder : (α : Type ?u.2063) → [inst : LE α Type ?u.2063 α ] [ IsSimpleOrder α ] [ DecidableEq : Sort ?u.500 → Sort (max1?u.500) α ]
theorem univ : Finset.univ = {⊤ , ⊥ } univ : ( Finset.univ : Finset α ) = { ⊤ , ⊥ } := by
change Finset.map _ ( Finset.univ : Finset Bool ) = _
rw [ Fintype.univ_bool ]
simp only [ Finset.map_insert , Function.Embedding.coeFn_mk : ∀ {α : Sort ?u.1485} {β : Sort ?u.1486} (f : α → β i : Function.Injective f ↑{ toFun := f , inj' := i } = f , Finset.map_singleton : ∀ {α : Type ?u.1513} {β : Type ?u.1514} (f : α ↪ β a : α ), Finset.map f {a } = {↑f a } ] {↑IsSimpleOrder.equivBool .symmtrue , ↑IsSimpleOrder.equivBool .symmfalse } = {⊤ , ⊥ }
rfl
#align fintype.is_simple_order.univ Fintype.IsSimpleOrder.univ
theorem card : Fintype.card α = 2 :=
( Fintype.ofEquiv_card _ ). trans : ∀ {α : Sort ?u.2339} {a b c : α }, a = b b = c a = c trans Fintype.card_bool
#align fintype.is_simple_order.card Fintype.IsSimpleOrder.card
end IsSimpleOrder
end Fintype
namespace Bool
instance : IsSimpleOrder Bool :=
⟨ fun a => by
rw [ ← Finset.mem_singleton : ∀ {α : Type ?u.2868} {a b : α }, b ∈ {a } ↔ b = a , Or.comm : ∀ {a b : Prop }, a ∨ b ↔ b ∨ a , ← Finset.mem_insert , top_eq_true , bot_eq_false , ←
Fintype.univ_bool ]
apply Finset.mem_univ : ∀ {α : Type ?u.3101} [inst : Fintype α x : α ), x ∈ Finset.univ ⟩
end Bool
section Fintype
open Finset
-- see Note [lower instance priority]
instance ( priority := 100) Finite.to_isCoatomic [ PartialOrder : Type ?u.3143 → Type ?u.3143 α ] [ OrderTop : (α : Type ?u.3146) → [inst : LE α Type ?u.3146 α ] [ Finite α ] :
IsCoatomic α := by
refine' IsCoatomic.mk fun b => or_iff_not_imp_left : ∀ {a b : Prop }, a ∨ b ↔ ¬ a b . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun ht => _
obtain ⟨c, hc, hmax⟩ : ∃ a , a ∈ { x | b ≤ x ∧ x ≠ ⊤ ∧ ∀ (a' : α ), a' ∈ { x | b ≤ x ∧ x ≠ ⊤ id a ≤ id a' id a = id a' c ⟨c, hc, hmax⟩ : ∃ a , a ∈ { x | b ≤ x ∧ x ≠ ⊤ ∧ ∀ (a' : α ), a' ∈ { x | b ≤ x ∧ x ≠ ⊤ id a ≤ id a' id a = id a' hc : c ∈ { x | b ≤ x ∧ x ≠ ⊤ hc ⟨c, hc, hmax⟩ : ∃ a , a ∈ { x | b ≤ x ∧ x ≠ ⊤ ∧ ∀ (a' : α ), a' ∈ { x | b ≤ x ∧ x ≠ ⊤ id a ≤ id a' id a = id a' hmax ⟨c, hc, hmax⟩ : ∃ a , a ∈ { x | b ≤ x ∧ x ≠ ⊤ ∧ ∀ (a' : α ), a' ∈ { x | b ≤ x ∧ x ≠ ⊤ id a ≤ id a' id a = id a' :=
Set.Finite.exists_maximal_wrt id : {α : Sort ?u.3338} → α → α { x : α | b ≤ x ∧ x ≠ ⊤ } ( Set.toFinite _ ) ⟨ b , le_rfl , ht ⟩
refine' ⟨ c , ⟨ hc : c ∈ { x | b ≤ x ∧ x ≠ ⊤ hc . 2 : ∀ {a b : Prop }, a ∧ b b , fun y hcy => _ ⟩, hc : c ∈ { x | b ≤ x ∧ x ≠ ⊤ hc . 1 : ∀ {a b : Prop }, a ∧ b a ⟩
by_contra hyt
obtain rfl : c = y := hmax y ⟨ hc : c ∈ { x | b ≤ x ∧ x ≠ ⊤ hc . 1 : ∀ {a b : Prop }, a ∧ b a . trans : ∀ {α : Type ?u.4276} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c trans hcy . le , hyt ⟩ hcy . le
exact ( lt_self_iff_false _ ). mp : ∀ {a b : Prop }, (a ↔ b a → b mp hcy
#align finite.to_is_coatomic Finite.to_isCoatomic
-- see Note [lower instance priority]
instance ( priority := 100) Finite.to_isAtomic [ PartialOrder : Type ?u.4438 → Type ?u.4438 α ] [ OrderBot : (α : Type ?u.4441) → [inst : LE α Type ?u.4441 α ] [ Finite α ] :
IsAtomic α :=
isCoatomic_dual_iff_isAtomic . mp : ∀ {a b : Prop }, (a ↔ b a → b Finite.to_isCoatomic
#align finite.to_is_atomic Finite.to_isAtomic
end Fintype